Theorem ndbier-P3.15 180

Description: Natural Deduction: '↔' Elimination Rule - Reverse Implication.

After deducing a biconditional statement, we can deduce the associated reverse implication.

Hypothesis

Ref	Expression
ndbier-P3.15.1	⊢ (𝛾 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ndbier-P3.15	⊢ (𝛾 → (𝜓 → 𝜑))

Proof of Theorem ndbier-P3.15

Step	Hyp	Ref	Expression
1		ndbier-P3.15.1	. 2 ⊢ (𝛾 → (𝜑 ↔ 𝜓))
2	1	birev-P2.5b.AC.SH 117	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-NDBIER0  241  ndbier-P3.15.CL  250  bisym-P3.33b  298  bitrns-P3.33c  302  subneg-P3.39  323  subiml-P3.40a  325  subimr-P3.40b  327  subimd-P3.40c  329  bimpr-P4  533  suballv-P5  623  subexv-P5  624  cbvallv-P5  659  specw-P5  661  cbvall-P6  751  suball-P6  753  subex-P6  754  lemma-L6.07a-L2  771  splitelof-P6-L1  777  lemma-L7.02a-L1  943  nfrgencl-P7  965  suball-P7  973  dfpsubv-P7  977  subex-P7  1042