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  1458  ax16  1836  ax16i  1881  nelneq  2306  nelneq2  2307  nelne1  2466  nelne2  2467  spc2gv  2864  spc3gv  2866  nssne1  3251  nssne2  3252  ifbothdc  3605  difsn  3770  iununir  4011  nbrne1  4064  nbrne2  4065  ss1o0el1  4242  mosubopt  4741  issref  5066  ssimaex  5642  chfnrn  5693  ffnfv  5740  f1elima  5844  dftpos4  6351  tfr1onlemsucaccv  6429  tfrcllemsucaccv  6442  snon0  7039  exmidonfinlem  7303  enq0sym  7547  prop  7590  prubl  7601  negf1o  8456  0fz1  10169  elfzmlbp  10256  swrdnd  11115  maxleast  11557  negfi  11572  isprm2  12472  nprmdvds1  12495  oddprmdvds  12710  exmidsbthrlem  15998