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  1457  ax16  1835  ax16i  1880  nelneq  2305  nelneq2  2306  nelne1  2465  nelne2  2466  spc2gv  2863  spc3gv  2865  nssne1  3250  nssne2  3251  ifbothdc  3604  difsn  3769  iununir  4010  nbrne1  4062  nbrne2  4063  ss1o0el1  4240  mosubopt  4739  issref  5064  ssimaex  5639  chfnrn  5690  ffnfv  5737  f1elima  5841  dftpos4  6348  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  snon0  7036  exmidonfinlem  7300  enq0sym  7544  prop  7587  prubl  7598  negf1o  8453  0fz1  10166  elfzmlbp  10253  maxleast  11495  negfi  11510  isprm2  12410  nprmdvds1  12433  oddprmdvds  12648  exmidsbthrlem  15923