Theorem biimpcd 158

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 154	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpac  296  3impexpbicom  1415  ax16  1786  ax16i  1831  nelneq  2241  nelneq2  2242  nelne1  2399  nelne2  2400  spc2gv  2780  spc3gv  2782  nssne1  3160  nssne2  3161  ifbothdc  3509  difsn  3665  iununir  3904  nbrne1  3955  nbrne2  3956  exmid01  4129  mosubopt  4612  issref  4929  ssimaex  5490  chfnrn  5539  ffnfv  5586  f1elima  5682  dftpos4  6168  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  snon0  6832  exmidonfinlem  7066  enq0sym  7264  prop  7307  prubl  7318  negf1o  8168  0fz1  9856  elfzmlbp  9940  maxleast  11017  negfi  11031  isprm2  11834  nprmdvds1  11856  exmidsbthrlem  13392