Theorem ndbii-P3.13 178

Description: Natural Deduction: '↔' Introduction Rule.

If we have previously deduced both directions of a biconditional, then we can deduce the full biconditional.

Hypotheses

Ref	Expression
ndbii-P3.13.1	⊢ (𝛾 → (𝜑 → 𝜓))
ndbii-P3.13.2	⊢ (𝛾 → (𝜓 → 𝜑))

Assertion

Ref	Expression
ndbii-P3.13	⊢ (𝛾 → (𝜑 ↔ 𝜓))

Proof of Theorem ndbii-P3.13

Step	Hyp	Ref	Expression
1		ndbii-P3.13.1	. 2 ⊢ (𝛾 → (𝜑 → 𝜓))
2		ndbii-P3.13.2	. 2 ⊢ (𝛾 → (𝜓 → 𝜑))
3	1, 2	bicmb-P2.5c.AC.2SH 121	1 ⊢ (𝛾 → (𝜑 ↔ 𝜓))

Syntax hints:   → wff-imp 10   ↔ wff-bi 104

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

This theorem is referenced by:  rcp-NDBII0  239  ndbii-P3.13.CL  248  bisym-P3.33b  298  bitrns-P3.33c  302  subneg-P3.39  323  subiml-P3.40a  325  subimr-P3.40b  327  subimd-P3.40c  329  subbil-P3.41a  332  subandl-P3.42a  339  suborl-P3.43a  346  oroverbiint-P4.28d  471  biasandorint-P4.34b  492  suballv-P5  623  subexv-P5  624  subeql-P5  632  subeqr-P5  635  subelofl-P5  638  subelofr-P5  640  lemma-L6.01a  724  suball-P6  753  subex-P6  754  spliteq-P6-L1  775  splitelof-P6-L1  777  qremexd-P6  823  gennfrcl-P7  963  suball-P7  973  subex-P7  1042