Theorem biimpcd 157

Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimpcd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpcd	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibcom 153	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biimpac  292  3impexpbicom  1372  ax16  1741  ax16i  1786  nelneq  2188  nelneq2  2189  nelne1  2345  nelne2  2346  spc2gv  2709  spc3gv  2711  nssne1  3082  nssne2  3083  ifbothdc  3423  difsn  3574  iununir  3812  nbrne1  3862  nbrne2  3863  exmid01  4032  mosubopt  4503  issref  4814  ssimaex  5365  chfnrn  5410  ffnfv  5456  f1elima  5552  dftpos4  6028  tfr1onlemsucaccv  6106  tfrcllemsucaccv  6119  snon0  6643  enq0sym  6989  prop  7032  prubl  7043  negf1o  7858  0fz1  9457  elfzmlbp  9539  maxleast  10642  negfi  10655  isprm2  11373  nprmdvds1  11395  exmidsbthrlem  11867