Theorem biimpcd 158

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

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpac  296  3impexpbicom  1431  ax16  1806  ax16i  1851  nelneq  2271  nelneq2  2272  nelne1  2430  nelne2  2431  spc2gv  2821  spc3gv  2823  nssne1  3205  nssne2  3206  ifbothdc  3558  difsn  3717  iununir  3956  nbrne1  4008  nbrne2  4009  ss1o0el1  4183  mosubopt  4676  issref  4993  ssimaex  5557  chfnrn  5607  ffnfv  5654  f1elima  5752  dftpos4  6242  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  snon0  6913  exmidonfinlem  7170  enq0sym  7394  prop  7437  prubl  7448  negf1o  8301  0fz1  10001  elfzmlbp  10088  maxleast  11177  negfi  11191  isprm2  12071  nprmdvds1  12094  oddprmdvds  12306  exmidsbthrlem  14054