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  1458  ax16  1836  ax16i  1881  nelneq  2306  nelneq2  2307  nelne1  2466  nelne2  2467  spc2gv  2864  spc3gv  2866  nssne1  3251  nssne2  3252  ifbothdc  3605  difsn  3770  iununir  4011  nbrne1  4063  nbrne2  4064  ss1o0el1  4241  mosubopt  4740  issref  5065  ssimaex  5640  chfnrn  5691  ffnfv  5738  f1elima  5842  dftpos4  6349  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  snon0  7037  exmidonfinlem  7301  enq0sym  7545  prop  7588  prubl  7599  negf1o  8454  0fz1  10167  elfzmlbp  10254  swrdnd  11112  maxleast  11524  negfi  11539  isprm2  12439  nprmdvds1  12462  oddprmdvds  12677  exmidsbthrlem  15961