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  6594  eroveu  6905  fundmen  7100  nneneq  7164  fidifsnen  7178  prarloclem5  7873  prarloc  7876  recexprlemss1l  8008  recexprlemss1u  8009  uzin  9970  indstr  10008  elfzmlbp  10555  swrdnd  11452  isclwwlknx  16879