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  2852  spc3gv  2854  nssne1  3238  nssne2  3239  ifbothdc  3591  difsn  3756  iununir  3997  nbrne1  4049  nbrne2  4050  ss1o0el1  4227  mosubopt  4725  issref  5049  ssimaex  5619  chfnrn  5670  ffnfv  5717  f1elima  5817  dftpos4  6318  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  snon0  6996  exmidonfinlem  7255  enq0sym  7494  prop  7537  prubl  7548  negf1o  8403  0fz1  10114  elfzmlbp  10201  maxleast  11360  negfi  11374  isprm2  12258  nprmdvds1  12281  oddprmdvds  12495  exmidsbthrlem  15582