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  984  ax11i  1762  equsex  1776  eleq1a  2304  ceqsalg  2841  cgsexg  2848  cgsex2g  2849  cgsex4g  2850  ceqsex  2851  spc2egv  2906  spc3egv  2908  csbiebt  3177  dfiin2g  4023  sotricim  4443  ralxfrALT  4587  iunpw  4600  opelxp  4778  ssrel  4837  ssrel2  4839  ssrelrel  4849  iss  5083  funcnvuni  5424  fun11iun  5634  tfrlem8  6548  eroveu  6859  fundmen  7046  nneneq  7110  fidifsnen  7124  prarloclem5  7811  prarloc  7814  recexprlemss1l  7946  recexprlemss1u  7947  uzin  9883  indstr  9921  elfzmlbp  10462  swrdnd  11344  isclwwlknx  16398