Theorem biimprcd 216

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 213	1 |- (ch -> (ph -> ps))

Syntax hints:   -> wi 4   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  biimparc  473  ax11i  1647  ax11eq  2193  ax11el  2194  eleq1a  2422  ceqsalg  2884  cgsexg  2891  cgsex2g  2892  cgsex4g  2893  ceqsex  2894  spc2egv  2942  spc3egv  2944  csbiebt  3173  dfiin2g  4001  eqpw1uni  4331  sfintfin  4533  tfinnn  4535  sfinltfin  4536  funcnvuni  5162  fun11iun  5306  funsi  5521  fundmen  6044  dmfrec  6317