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  1481  ax16  1859  ax16i  1904  nelneq  2330  nelneq2  2331  nelne1  2490  nelne2  2491  spc2gv  2894  spc3gv  2896  nssne1  3282  nssne2  3283  ifbothdc  3637  ifpprsnssdc  3774  difsn  3805  iununir  4049  nbrne1  4102  nbrne2  4103  ss1o0el1  4281  mosubopt  4784  issref  5111  ssimaex  5697  chfnrn  5748  ffnfv  5795  f1elima  5903  dftpos4  6415  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  snon0  7113  en2prde  7377  exmidonfinlem  7382  enq0sym  7630  prop  7673  prubl  7684  negf1o  8539  0fz1  10253  elfzmlbp  10340  swrdnd  11206  maxleast  11739  negfi  11754  isprm2  12654  nprmdvds1  12677  oddprmdvds  12892  ushgredgedg  16039  ushgredgedgloop  16041  exmidsbthrlem  16450