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  1824  ax16i  1869  nelneq  2294  nelneq2  2295  nelne1  2454  nelne2  2455  spc2gv  2851  spc3gv  2853  nssne1  3237  nssne2  3238  ifbothdc  3590  difsn  3755  iununir  3996  nbrne1  4048  nbrne2  4049  ss1o0el1  4226  mosubopt  4724  issref  5048  ssimaex  5618  chfnrn  5669  ffnfv  5716  f1elima  5816  dftpos4  6316  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  snon0  6994  exmidonfinlem  7253  enq0sym  7492  prop  7535  prubl  7546  negf1o  8401  0fz1  10111  elfzmlbp  10198  maxleast  11357  negfi  11371  isprm2  12255  nprmdvds1  12278  oddprmdvds  12492  exmidsbthrlem  15512