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  difsn  3804  iununir  4048  nbrne1  4101  nbrne2  4102  ss1o0el1  4280  mosubopt  4783  issref  5110  ssimaex  5694  chfnrn  5745  ffnfv  5792  f1elima  5896  dftpos4  6407  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  snon0  7098  en2prde  7362  exmidonfinlem  7367  enq0sym  7615  prop  7658  prubl  7669  negf1o  8524  0fz1  10237  elfzmlbp  10324  swrdnd  11186  maxleast  11719  negfi  11734  isprm2  12634  nprmdvds1  12657  oddprmdvds  12872  ushgredgedg  16018  ushgredgedgloop  16020  exmidsbthrlem  16349