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  1484  ax16  1862  ax16i  1907  nelneq  2333  nelneq2  2334  nelne1  2502  nelne2  2503  spc2gv  2908  spc3gv  2910  nssne1  3296  nssne2  3297  ifbothdc  3657  ifpprsnssdc  3799  difsn  3831  iununir  4075  nbrne1  4128  nbrne2  4129  ss1o0el1  4310  mosubopt  4815  issref  5145  ssimaex  5738  chfnrn  5789  ffnfv  5835  f1elima  5946  dftpos4  6494  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  snon0  7202  en2prde  7490  exmidonfinlem  7496  enq0sym  7747  prop  7790  prubl  7801  negf1o  8655  0fz1  10379  elfzmlbp  10466  swrdnd  11351  maxleast  11898  negfi  11913  isprm2  12814  nprmdvds1  12837  oddprmdvds  13052  ushgredgedg  16221  ushgredgedgloop  16223  loopclwwlkn1b  16414  clwwlkext2edg  16417  eupth2lem3lem4fi  16468  exmidsbthrlem  16802