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  1481  ax16  1859  ax16i  1904  nelneq  2330  nelneq2  2331  nelne1  2490  nelne2  2491  spc2gv  2895  spc3gv  2897  nssne1  3283  nssne2  3284  ifbothdc  3638  ifpprsnssdc  3777  difsn  3808  iununir  4052  nbrne1  4105  nbrne2  4106  ss1o0el1  4285  mosubopt  4789  issref  5117  ssimaex  5703  chfnrn  5754  ffnfv  5801  f1elima  5909  dftpos4  6424  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  snon0  7125  en2prde  7389  exmidonfinlem  7394  enq0sym  7642  prop  7685  prubl  7696  negf1o  8551  0fz1  10270  elfzmlbp  10357  swrdnd  11230  maxleast  11764  negfi  11779  isprm2  12679  nprmdvds1  12702  oddprmdvds  12917  ushgredgedg  16065  ushgredgedgloop  16067  loopclwwlkn1b  16214  clwwlkext2edg  16217  exmidsbthrlem  16562