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  1414  ax16  1785  ax16i  1830  nelneq  2240  nelneq2  2241  nelne1  2398  nelne2  2399  spc2gv  2776  spc3gv  2778  nssne1  3155  nssne2  3156  ifbothdc  3504  difsn  3657  iununir  3896  nbrne1  3947  nbrne2  3948  exmid01  4121  mosubopt  4604  issref  4921  ssimaex  5482  chfnrn  5531  ffnfv  5578  f1elima  5674  dftpos4  6160  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  snon0  6824  exmidonfinlem  7049  enq0sym  7240  prop  7283  prubl  7294  negf1o  8144  0fz1  9825  elfzmlbp  9909  maxleast  10985  negfi  10999  isprm2  11798  nprmdvds1  11820  exmidsbthrlem  13217