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  1488  ax16  1866  ax16i  1911  nelneq  2339  nelneq2  2340  nelne1  2510  nelne2  2511  spc2gv  2916  spc3gv  2918  nssne1  3306  nssne2  3307  ifbothdc  3672  ifpprsnssdc  3815  difsn  3847  iununir  4091  nbrne1  4144  nbrne2  4145  ss1o0el1  4329  mosubopt  4835  issref  5165  ssimaex  5758  chfnrn  5811  ffnfv  5857  f1elima  5969  dftpos4  6524  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  snon0  7239  en2prde  7529  exmidonfinlem  7535  enq0sym  7789  prop  7832  prubl  7843  negf1o  8699  0fz1  10428  elfzmlbp  10517  swrdnd  11409  maxleast  11957  negfi  11972  isprm2  12873  nprmdvds1  12896  oddprmdvds  13111  ushgredgedg  16381  ushgredgedgloop  16383  loopclwwlkn1b  16574  clwwlkext2edg  16577  eupth2lem3lem4fi  16628  exmidsbthrlem  16972