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  1367  ax16  1734  ax16i  1779  nelneq  2179  nelneq2  2180  nelne1  2335  nelne2  2336  spc2gv  2688  spc3gv  2690  nssne1  3055  nssne2  3056  ifbothdc  3380  difsn  3523  iununir  3759  nbrne1  3802  nbrne2  3803  mosubopt  4423  issref  4727  ssimaex  5255  chfnrn  5299  ffnfv  5344  f1elima  5433  dftpos4  5901  snon0  6387  enq0sym  6622  prop  6665  prubl  6676  negf1o  7486  0fz1  9064  elfzmlbp  9143  maxleast  10099  negfi  10110  isprm2  10499  nprmdvds1  10521