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  1436  ax16  1811  ax16i  1856  nelneq  2276  nelneq2  2277  nelne1  2435  nelne2  2436  spc2gv  2826  spc3gv  2828  nssne1  3211  nssne2  3212  ifbothdc  3564  difsn  3726  iununir  3965  nbrne1  4017  nbrne2  4018  ss1o0el1  4192  mosubopt  4685  issref  5003  ssimaex  5569  chfnrn  5619  ffnfv  5666  f1elima  5764  dftpos4  6254  tfr1onlemsucaccv  6332  tfrcllemsucaccv  6345  snon0  6925  exmidonfinlem  7182  enq0sym  7406  prop  7449  prubl  7460  negf1o  8313  0fz1  10013  elfzmlbp  10100  maxleast  11188  negfi  11202  isprm2  12082  nprmdvds1  12105  oddprmdvds  12317  exmidsbthrlem  14329