Theorem ndbief-P3.14 179

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

After deducing a biconditional statement, we can deduce the assocated forward implication.

Hypothesis

Ref	Expression
ndbief-P3.14.1	⊢ (𝛾 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ndbief-P3.14	⊢ (𝛾 → (𝜑 → 𝜓))

Proof of Theorem ndbief-P3.14

Step	Hyp	Ref	Expression
1		ndbief-P3.14.1	. 2 ⊢ (𝛾 → (𝜑 ↔ 𝜓))
2	1	bifwd-P2.5a.AC.SH 113	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-NDBIEF0  240  ndbief-P3.14.CL  249  bisym-P3.33b  298  bitrns-P3.33c  302  subneg-P3.39  323  subiml-P3.40a  325  subimr-P3.40b  327  subimd-P3.40c  329  subandl-P3.42a-L1  338  suborl-P3.43a-L1  345  negbicancel-P4.11  419  negbicancelint-P4.14  424  bimpf-P4  531  subneg2-P4  538  subiml2-P4  540  subimr2-P4  542  subimd2-P4  544  subbil2-P4  546  subbir2-P4  548  subbid2-P4  550  subandl2-P4  552  subandr2-P4  554  subandd2-P4  556  suborl2-P4  558  suborr2-P4  560  subord2-P4  562  suballv-P5  623  subexv-P5  624  specisub-P5  654  cbvallv-P5  659  cbvall-P6  751  suball-P6  753  subex-P6  754  lemma-L6.07a-L1  770  splitelof-P6-L1  777  exiad-P6  824  lemma-L7.02a-L1  943  suball-P7  973  dfpsubv-P7  977  axL12-P7  982  subex-P7  1042