Theorem biimpcd 159

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 155	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimpac  298  3impexpbicom  1438  ax16  1813  ax16i  1858  nelneq  2278  nelneq2  2279  nelne1  2437  nelne2  2438  spc2gv  2828  spc3gv  2830  nssne1  3213  nssne2  3214  ifbothdc  3567  difsn  3729  iununir  3970  nbrne1  4022  nbrne2  4023  ss1o0el1  4197  mosubopt  4691  issref  5011  ssimaex  5577  chfnrn  5627  ffnfv  5674  f1elima  5773  dftpos4  6263  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  snon0  6934  exmidonfinlem  7191  enq0sym  7430  prop  7473  prubl  7484  negf1o  8338  0fz1  10044  elfzmlbp  10131  maxleast  11221  negfi  11235  isprm2  12116  nprmdvds1  12139  oddprmdvds  12351  exmidsbthrlem  14740