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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimparc  299  pm5.32  457  oplem1  988  ax11i  1766  equsex  1780  eleq1a  2310  ceqsalg  2850  cgsexg  2857  cgsex2g  2858  cgsex4g  2859  ceqsex  2860  spc2egv  2915  spc3egv  2917  csbiebt  3187  dfiin2g  4045  sotricim  4470  ralxfrALT  4615  iunpw  4628  opelxp  4806  ssrel  4865  ssrel2  4867  ssrelrel  4877  iss  5112  funcnvuni  5453  fun11iun  5663  tfrlem8  6593  eroveu  6904  fundmen  7098  nneneq  7162  fidifsnen  7176  prarloclem5  7873  prarloc  7876  recexprlemss1l  8008  recexprlemss1u  8009  uzin  9971  indstr  10009  elfzmlbp  10556  swrdnd  11453  isclwwlknx  16862