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  2589  rspcimdv  2957  rspcedv  2960  moi2  3018  moi  3020  sspsstr  3375  unsneqsn  3888  opkth1g  4131  peano5  4410  ssfin  4471  tfincl  4493  sucoddeven  4512  eventfin  4518  oddtfin  4519  spfininduct  4541  vfinspeqtncv  4554  iss  5001  tz6.12c  5348  fveqres  5356  fvun1  5380  fvopab3ig  5388  dffo4  5424  fconst5  5456  ndmovordi  5622  clos1induct  5881  enprmaplem3  6079  enprmaplem5  6081  leconnnc  6219  nchoicelem12  6301