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  980  ax11i  1740  equsex  1754  eleq1a  2281  ceqsalg  2808  cgsexg  2815  cgsex2g  2816  cgsex4g  2817  ceqsex  2818  spc2egv  2873  spc3egv  2875  csbiebt  3144  dfiin2g  3977  sotricim  4391  ralxfrALT  4535  iunpw  4548  opelxp  4726  ssrel  4784  ssrel2  4786  ssrelrel  4796  iss  5027  funcnvuni  5366  fun11iun  5569  tfrlem8  6434  eroveu  6743  fundmen  6929  nneneq  6986  fidifsnen  7000  prarloclem5  7655  prarloc  7658  recexprlemss1l  7790  recexprlemss1u  7791  uzin  9723  indstr  9756  elfzmlbp  10296  swrdnd  11157