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  977  ax11i  1725  equsex  1739  eleq1a  2265  ceqsalg  2788  cgsexg  2795  cgsex2g  2796  cgsex4g  2797  ceqsex  2798  spc2egv  2851  spc3egv  2853  csbiebt  3121  dfiin2g  3946  sotricim  4355  ralxfrALT  4499  iunpw  4512  opelxp  4690  ssrel  4748  ssrel2  4750  ssrelrel  4760  iss  4989  funcnvuni  5324  fun11iun  5522  tfrlem8  6373  eroveu  6682  fundmen  6862  nneneq  6915  fidifsnen  6928  prarloclem5  7562  prarloc  7565  recexprlemss1l  7697  recexprlemss1u  7698  uzin  9628  indstr  9661  elfzmlbp  10201