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  981  ax11i  1760  equsex  1774  eleq1a  2301  ceqsalg  2829  cgsexg  2836  cgsex2g  2837  cgsex4g  2838  ceqsex  2839  spc2egv  2894  spc3egv  2896  csbiebt  3165  dfiin2g  4001  sotricim  4418  ralxfrALT  4562  iunpw  4575  opelxp  4753  ssrel  4812  ssrel2  4814  ssrelrel  4824  iss  5057  funcnvuni  5396  fun11iun  5601  tfrlem8  6479  eroveu  6790  fundmen  6976  nneneq  7038  fidifsnen  7052  prarloclem5  7713  prarloc  7716  recexprlemss1l  7848  recexprlemss1u  7849  uzin  9782  indstr  9820  elfzmlbp  10360  swrdnd  11233  isclwwlknx  16225