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  1368  ax16  1735  ax16i  1780  nelneq  2180  nelneq2  2181  nelne1  2336  nelne2  2337  spc2gv  2689  spc3gv  2691  nssne1  3056  nssne2  3057  ifbothdc  3382  difsn  3525  iununir  3761  nbrne1  3804  nbrne2  3805  mosubopt  4425  issref  4731  ssimaex  5260  chfnrn  5304  ffnfv  5349  f1elima  5438  dftpos4  5906  tfr1onlemsucaccv  5984  tfrcllemsucaccv  5997  snon0  6435  enq0sym  6673  prop  6716  prubl  6727  negf1o  7542  0fz1  9129  elfzmlbp  9209  maxleast  10226  negfi  10237  isprm2  10632  nprmdvds1  10654