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  975  ax11i  1714  equsex  1728  eleq1a  2249  ceqsalg  2767  cgsexg  2774  cgsex2g  2775  cgsex4g  2776  ceqsex  2777  spc2egv  2829  spc3egv  2831  csbiebt  3098  dfiin2g  3921  sotricim  4325  ralxfrALT  4469  iunpw  4482  opelxp  4658  ssrel  4716  ssrel2  4718  ssrelrel  4728  iss  4955  funcnvuni  5287  fun11iun  5484  tfrlem8  6321  eroveu  6628  fundmen  6808  nneneq  6859  fidifsnen  6872  prarloclem5  7501  prarloc  7504  recexprlemss1l  7636  recexprlemss1u  7637  uzin  9562  indstr  9595  elfzmlbp  10134