Theorem biimprcd 160

Description: Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)

Hypothesis

Ref	Expression
biimpcd.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimprcd	|- ( ch -> ( ph -> ps ) )

Proof of Theorem biimprcd

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ch -> ch )
2		biimpcd.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5ibrcom 157	1 |- ( ch -> ( ph -> ps ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimparc  299  pm5.32  453  oplem1  983  ax11i  1762  equsex  1776  eleq1a  2303  ceqsalg  2831  cgsexg  2838  cgsex2g  2839  cgsex4g  2840  ceqsex  2841  spc2egv  2896  spc3egv  2898  csbiebt  3167  dfiin2g  4003  sotricim  4420  ralxfrALT  4564  iunpw  4577  opelxp  4755  ssrel  4814  ssrel2  4816  ssrelrel  4826  iss  5059  funcnvuni  5399  fun11iun  5604  tfrlem8  6484  eroveu  6795  fundmen  6981  nneneq  7043  fidifsnen  7057  prarloclem5  7720  prarloc  7723  recexprlemss1l  7855  recexprlemss1u  7856  uzin  9789  indstr  9827  elfzmlbp  10367  swrdnd  11241  isclwwlknx  16270