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  2830  spc3gv  2832  nssne1  3215  nssne2  3216  ifbothdc  3569  difsn  3731  iununir  3972  nbrne1  4024  nbrne2  4025  ss1o0el1  4199  mosubopt  4693  issref  5013  ssimaex  5579  chfnrn  5629  ffnfv  5676  f1elima  5776  dftpos4  6266  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  snon0  6937  exmidonfinlem  7194  enq0sym  7433  prop  7476  prubl  7487  negf1o  8341  0fz1  10047  elfzmlbp  10134  maxleast  11224  negfi  11238  isprm2  12119  nprmdvds1  12142  oddprmdvds  12354  exmidsbthrlem  14855