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  1438  ax16  1813  ax16i  1858  nelneq  2278  nelneq2  2279  nelne1  2437  nelne2  2438  spc2gv  2828  spc3gv  2830  nssne1  3213  nssne2  3214  ifbothdc  3567  difsn  3729  iununir  3968  nbrne1  4020  nbrne2  4021  ss1o0el1  4195  mosubopt  4689  issref  5008  ssimaex  5574  chfnrn  5624  ffnfv  5671  f1elima  5769  dftpos4  6259  tfr1onlemsucaccv  6337  tfrcllemsucaccv  6350  snon0  6930  exmidonfinlem  7187  enq0sym  7426  prop  7469  prubl  7480  negf1o  8333  0fz1  10038  elfzmlbp  10125  maxleast  11213  negfi  11227  isprm2  12107  nprmdvds1  12130  oddprmdvds  12342  exmidsbthrlem  14541