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  1449  ax16  1827  ax16i  1872  nelneq  2297  nelneq2  2298  nelne1  2457  nelne2  2458  spc2gv  2855  spc3gv  2857  nssne1  3242  nssne2  3243  ifbothdc  3595  difsn  3760  iununir  4001  nbrne1  4053  nbrne2  4054  ss1o0el1  4231  mosubopt  4729  issref  5053  ssimaex  5625  chfnrn  5676  ffnfv  5723  f1elima  5823  dftpos4  6330  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  snon0  7010  exmidonfinlem  7274  enq0sym  7518  prop  7561  prubl  7572  negf1o  8427  0fz1  10139  elfzmlbp  10226  maxleast  11397  negfi  11412  isprm2  12312  nprmdvds1  12335  oddprmdvds  12550  exmidsbthrlem  15779