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  2211  ceqsalg  2714  cgsexg  2721  cgsex2g  2722  cgsex4g  2723  ceqsex  2724  spc2egv  2775  spc3egv  2777  csbiebt  3039  dfiin2g  3846  sotricim  4245  ralxfrALT  4388  iunpw  4401  opelxp  4569  ssrel  4627  ssrel2  4629  ssrelrel  4639  iss  4865  funcnvuni  5192  fun11iun  5388  tfrlem8  6215  eroveu  6520  fundmen  6700  nneneq  6751  fidifsnen  6764  prarloclem5  7308  prarloc  7311  recexprlemss1l  7443  recexprlemss1u  7444  uzin  9358  indstr  9388  elfzmlbp  9909