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	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimpcd	|- ( ps -> ( ph -> ch ) )

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2		biimpcd.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5ibcom 155	1 |- ( ps -> ( ph -> ch ) )

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  2894  spc3gv  2896  nssne1  3282  nssne2  3283  ifbothdc  3637  ifpprsnssdc  3774  difsn  3805  iununir  4049  nbrne1  4102  nbrne2  4103  ss1o0el1  4281  mosubopt  4784  issref  5111  ssimaex  5695  chfnrn  5746  ffnfv  5793  f1elima  5897  dftpos4  6409  tfr1onlemsucaccv  6487  tfrcllemsucaccv  6500  snon0  7102  en2prde  7366  exmidonfinlem  7371  enq0sym  7619  prop  7662  prubl  7673  negf1o  8528  0fz1  10241  elfzmlbp  10328  swrdnd  11191  maxleast  11724  negfi  11739  isprm2  12639  nprmdvds1  12662  oddprmdvds  12877  ushgredgedg  16024  ushgredgedgloop  16026  exmidsbthrlem  16390