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  1459  ax16  1837  ax16i  1882  nelneq  2308  nelneq2  2309  nelne1  2468  nelne2  2469  spc2gv  2871  spc3gv  2873  nssne1  3259  nssne2  3260  ifbothdc  3614  difsn  3781  iununir  4025  nbrne1  4078  nbrne2  4079  ss1o0el1  4257  mosubopt  4758  issref  5084  ssimaex  5663  chfnrn  5714  ffnfv  5761  f1elima  5865  dftpos4  6372  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  snon0  7063  en2prde  7327  exmidonfinlem  7332  enq0sym  7580  prop  7623  prubl  7634  negf1o  8489  0fz1  10202  elfzmlbp  10289  swrdnd  11150  maxleast  11639  negfi  11654  isprm2  12554  nprmdvds1  12577  oddprmdvds  12792  exmidsbthrlem  16163