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  1761  equsex  1775  eleq1a  2302  ceqsalg  2830  cgsexg  2837  cgsex2g  2838  cgsex4g  2839  ceqsex  2840  spc2egv  2895  spc3egv  2897  csbiebt  3166  dfiin2g  4004  sotricim  4422  ralxfrALT  4566  iunpw  4579  opelxp  4757  ssrel  4816  ssrel2  4818  ssrelrel  4828  iss  5061  funcnvuni  5401  fun11iun  5607  tfrlem8  6489  eroveu  6800  fundmen  6986  nneneq  7048  fidifsnen  7062  prarloclem5  7725  prarloc  7728  recexprlemss1l  7860  recexprlemss1u  7861  uzin  9794  indstr  9832  elfzmlbp  10372  swrdnd  11249  isclwwlknx  16296