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  977  ax11i  1725  equsex  1739  eleq1a  2265  ceqsalg  2788  cgsexg  2795  cgsex2g  2796  cgsex4g  2797  ceqsex  2798  spc2egv  2850  spc3egv  2852  csbiebt  3120  dfiin2g  3945  sotricim  4354  ralxfrALT  4498  iunpw  4511  opelxp  4689  ssrel  4747  ssrel2  4749  ssrelrel  4759  iss  4988  funcnvuni  5323  fun11iun  5521  tfrlem8  6371  eroveu  6680  fundmen  6860  nneneq  6913  fidifsnen  6926  prarloclem5  7560  prarloc  7563  recexprlemss1l  7695  recexprlemss1u  7696  uzin  9625  indstr  9658  elfzmlbp  10198