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  1449  ax16  1827  ax16i  1872  nelneq  2297  nelneq2  2298  nelne1  2457  nelne2  2458  spc2gv  2855  spc3gv  2857  nssne1  3242  nssne2  3243  ifbothdc  3595  difsn  3760  iununir  4001  nbrne1  4053  nbrne2  4054  ss1o0el1  4231  mosubopt  4729  issref  5053  ssimaex  5625  chfnrn  5676  ffnfv  5723  f1elima  5823  dftpos4  6330  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  snon0  7010  exmidonfinlem  7272  enq0sym  7516  prop  7559  prubl  7570  negf1o  8425  0fz1  10137  elfzmlbp  10224  maxleast  11395  negfi  11410  isprm2  12310  nprmdvds1  12333  oddprmdvds  12548  exmidsbthrlem  15753