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  450  oplem1  970  ax11i  1707  equsex  1721  eleq1a  2242  ceqsalg  2758  cgsexg  2765  cgsex2g  2766  cgsex4g  2767  ceqsex  2768  spc2egv  2820  spc3egv  2822  csbiebt  3088  dfiin2g  3906  sotricim  4308  ralxfrALT  4452  iunpw  4465  opelxp  4641  ssrel  4699  ssrel2  4701  ssrelrel  4711  iss  4937  funcnvuni  5267  fun11iun  5463  tfrlem8  6297  eroveu  6604  fundmen  6784  nneneq  6835  fidifsnen  6848  prarloclem5  7462  prarloc  7465  recexprlemss1l  7597  recexprlemss1u  7598  uzin  9519  indstr  9552  elfzmlbp  10088