Theorem biimprd 214

Description: Deduce a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimprd.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biimprd	|- (ph -> (ch -> ps))

Proof of Theorem biimprd

Step	Hyp	Ref	Expression
1		id 19	. 2 |- (ch -> ch)
2		biimprd.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	syl5ibr 212	1 |- (ph -> (ch -> 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:  syl6bir  220  mpbird  223  sylibrd  225  sylbird  226  con4bid  284  mtbid  291  mtbii  293  imbi1d  308  biimpar  471  prlem1  928  spfw  1691  spw  1694  cbvalw  1701  cbvalvw  1702  alcomiw  1704  nfimd  1808  ax10lem2  1937  ax10lem4  1941  dral1  1965  cbval  1984  speiv  2000  ax16i  2046  a16gALT  2049  sbequi  2059  sb9i  2094  dral1-o  2154  a16g-o  2186  cleqh  2450  pm13.18  2588  rspcimdv  2956  rspcedv  2959  moi2  3017  moi  3019  sspsstr  3374  unsneqsn  3887  opkth1g  4130  peano5  4409  ssfin  4470  tfincl  4492  sucoddeven  4511  eventfin  4517  oddtfin  4518  spfininduct  4540  vfinspeqtncv  4553  iss  5000  tz6.12c  5347  fveqres  5355  fvun1  5379  fvopab3ig  5387  dffo4  5423  fconst5  5455  ndmovordi  5621  clos1induct  5880  enprmaplem3  6078  enprmaplem5  6080  leconnnc  6218  nchoicelem12  6300