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  1449  ax16  1827  ax16i  1872  nelneq  2297  nelneq2  2298  nelne1  2457  nelne2  2458  spc2gv  2855  spc3gv  2857  nssne1  3241  nssne2  3242  ifbothdc  3594  difsn  3759  iununir  4000  nbrne1  4052  nbrne2  4053  ss1o0el1  4230  mosubopt  4728  issref  5052  ssimaex  5622  chfnrn  5673  ffnfv  5720  f1elima  5820  dftpos4  6321  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  snon0  7001  exmidonfinlem  7260  enq0sym  7499  prop  7542  prubl  7553  negf1o  8408  0fz1  10120  elfzmlbp  10207  maxleast  11378  negfi  11393  isprm2  12285  nprmdvds1  12308  oddprmdvds  12523  exmidsbthrlem  15666