Theorem rcp-NDBII0 239

Description: '↔' Introduction. †

Hypotheses

Ref	Expression
rcp-NDBII0.1	⊢ (𝜑 → 𝜓)
rcp-NDBII0.2	⊢ (𝜓 → 𝜑)

Assertion

Ref	Expression
rcp-NDBII0	⊢ (𝜑 ↔ 𝜓)

Proof of Theorem rcp-NDBII0

Step	Hyp	Ref	Expression
1		rcp-NDBII0.1	. . . 4 ⊢ (𝜑 → 𝜓)
2	1	ndtruei-P3.17 182	. . 3 ⊢ (⊤ → (𝜑 → 𝜓))
3		rcp-NDBII0.2	. . . 4 ⊢ (𝜓 → 𝜑)
4	3	ndtruei-P3.17 182	. . 3 ⊢ (⊤ → (𝜓 → 𝜑))
5	2, 4	ndbii-P3.13 178	. 2 ⊢ (⊤ → (𝜑 ↔ 𝜓))
6	5	ndtruee-P3.18 183	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   → wff-imp 10   ↔ 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:  biref-P3.33a  297  bisym-P3.33b.CL.SYM  301  andcomm-P3.35  314  andassoc-P3.36  317  orcomm-P3.37  319  orassoc-P3.38  322  andasim-P3.46a  356  dfbi-P3.47  358  orasim-P3.48a  361  dffalse-P3.49  365  dnegeq-P4.10  418  dnegeqint-P4.13  423  idandtruel-P4.19a  438  idorfalsel-P4.20a  440  thmeqtrue-P4.21a  442  nthmeqfalse-P4.21b  443  trueie-P4.22a  444  falseie-P4.22b  445  idempotand-P4.25a  450  idempotor-P4.25b  451  dmorga-P4.26a  456  dmorgb-P4.26b  457  andoveror-P4.27a  461  oroverand-P4.27b  464  oroverim-P4.28a  467  imoverand-P4.29a  472  imoveror-P4.29b  474  imoverim-P4.30a  477  rimoverand-P4.31a  481  rimoveror-P4.31b  482  imasor-P4.32a  487  trnspeq-P4a  535  trnspeq-P4b  536  trnspeq-P4c  537  suballinf-P5  594  subexinf-P5  608  qimeqex-P5  612  qimeqallav-P5  618  qimeqallbv-P5  620  eqsym-P5.CL.SYM  629  qremallv-P5  656  qremexv-P5  657  cbvallv-P5  659  allcommw-P5  669  excommw-P5  670  qimeqalla-P6  699  qimeqallb-P6  701  qremallw-P6  702  qremexw-P6  703  qremall-P6  722  qremex-P6  723  allcomm-P6  739  cbvall-P6  751  lemma-L6.07a  772  psubim-P6  791  eqsym-P7.CL.SYM  938  allnegex-P7  958  dfnfreealt-P7  967  qimeqallb-P7  976  dfpsubv-P7  977  qimeqalla-P7  1050  qimeqex-P7  1056  allcomm-P7  1058  excomm-P7  1059  cbvall-P7  1061  cbvex-P7  1066  gennfr-P8  1079  exgennfr-P8  1085  idempotall-P8  1093  idempotex-P8  1094  idempotallex-P8  1095  idempotexall-P8  1096  idempotallnall-P8  1097  idempotexnex-P8  1098  idempotallnex-P8  1099  idempotexnall-P8  1100  qremall-P8  1101  qremex-P8  1103  qswap-P8  1105  nfrnegbi-P8  1113