Theorem bisym-P3.33b.RC 299

Description: Inference Form of bisym-P3.33b 298. †

Hypothesis

Ref	Expression
bisym-P3.33b.RC.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
bisym-P3.33b.RC	⊢ (𝜓 ↔ 𝜑)

Proof of Theorem bisym-P3.33b.RC

Step	Hyp	Ref	Expression
1		bisym-P3.33b.RC.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	ndtruei-P3.17 182	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	bisym-P3.33b 298	. 2 ⊢ (⊤ → (𝜓 ↔ 𝜑))
4	3	ndtruee-P3.18 183	1 ⊢ (𝜓 ↔ 𝜑)

Syntax hints:   ↔ wff-bi 104  ⊤wff-true 153

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem depends on definitions:  df-bi-D2.1 107  df-true-D2.4 155

This theorem is referenced by:  oroverim-P4.28-L1  465  oroverbi-P4.28b  469  imoverbi-P4.30b  479  imasand-P4.33a  489  truthtblnegt-P4.35a  493  peirce2exclmid-P4.41b  513  andassoc2b-P4  570  orassoc2b-P4  574  allnegex-P5  597  allasex-P5  599  qimeqallhalf-P5  609  qimeqex-P5-L1  610  cbvexv-P5  660  exiw-P5  662  qcallimrv-P5  671  qceximrv-P5  672  qcallimlv-P5  673  qceximlv-P5  674  genallw-P6  676  genexw-P6  677  dfnfreealt-P6  683  nfrleq-P6  687  nfrneg-P6  688  solvesub-P6a  704  example-E6.01a  706  example-E6.02a  712  dfpsubv-P6  717  spec-P6  719  specpsub-P6  721  psubtoisubv-P6  725  genex-P6  731  cbvex-P6  752  subnfr-P6  755  qcallimr-P6  757  qceximr-P6  758  qcalliml-P6  759  qceximl-P6  760  qcexandr-P6  761  qcexandl-P6  762  psubtoisub-P6  765  lemma-L6.07a-L2  771  psubleq-P6  783  psubneg-P6-L1  787  psubneg-P6  788  psubim-P6-L1  789  psubim-P6-L2  790  psuband-P6  792  psuball2v-P6  796  psubex2v-P6  797  gennfrcl-L6  812  nfrexgencl-L6  813  nfrimd-P6  815  nfrandd-P6  816  nfrord-P6  817  nfrbid-P6  818  ndalli-P6  822  psubnfrv-P7  927  nfrgen-P7  928  psubinv-P7  939  lemma-L7.02a-L1  943  exi-P7  951  dfexists-P7  959  lemma-L7.03  962  dfnfree-P7  968  allasex-P7  1048  qimeqex-P7-L1  1054  qcallimr-P8  1122  qceximr-P8  1123  qcalliml-P8  1124  qceximl-P8  1125