Theorem biimprcd 159

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 156	1 |- ( ch -> ( ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimparc  297  pm5.32  448  oplem1  959  ax11i  1692  equsex  1706  eleq1a  2209  ceqsalg  2709  cgsexg  2716  cgsex2g  2717  cgsex4g  2718  ceqsex  2719  spc2egv  2770  spc3egv  2772  csbiebt  3034  dfiin2g  3841  sotricim  4240  ralxfrALT  4383  iunpw  4396  opelxp  4564  ssrel  4622  ssrel2  4624  ssrelrel  4634  iss  4860  funcnvuni  5187  fun11iun  5381  tfrlem8  6208  eroveu  6513  fundmen  6693  nneneq  6744  fidifsnen  6757  prarloclem5  7301  prarloc  7304  recexprlemss1l  7436  recexprlemss1u  7437  uzin  9351  indstr  9381  elfzmlbp  9902