Theorem 2thd 240

Description: Two truths are equivalent (deduction rule). (Contributed by NM, 3-Jun-2012.)

Hypotheses

Ref	Expression
2thd.1	|- ( ph -> ps )
2thd.2	|- ( ph -> ch )

Assertion

Ref	Expression
2thd	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem 2thd

Step	Hyp	Ref	Expression
1		2thd.1	. 2 |- ( ph -> ps )
2		2thd.2	. 2 |- ( ph -> ch )
3		pm5.1im 238	. 2 |- ( ps -> ( ch -> ( ps <-> ch ) ) )
4	1, 2, 3	sylc 60	1 |- ( ph -> ( ps <-> ch ) )

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

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 185

This theorem is referenced by:  had1  1454  sbc2or  3340  abvor0  3803  ralidm  3931  disjprg  4443  euotd  4748  posn  5067  frsn  5069  cnvpo  5543  elabrex  6141  riota5f  6268  smoord  7033  brwdom2  7995  finacn  8427  acacni  8516  dfac13  8518  fin1a2lem10  8785  gch2  9049  gchac  9055  recmulnq  9338  nn1m1nn  10552  nn0sub  10842  qextltlem  11397  xsubge0  11449  xlesubadd  11451  iccshftr  11650  iccshftl  11652  iccdil  11654  icccntr  11656  fzaddel  11714  elfzomelpfzo  11878  sqlecan  12238  nnesq  12254  hashdom  12411  swrdspsleq  12632  repswsymballbi  12711  znnenlem  13802  bitsmod  13941  dvdssq  14053  pcdvdsb  14247  vdwmc2  14352  acsfn  14910  subsubc  15076  funcres2b  15120  isipodrs  15644  issubg3  16014  opnnei  19387  lmss  19565  lmres  19567  cmpfi  19674  xkopt  19891  acufl  20153  lmhmclm  21321  equivcmet  21489  degltlem1  22207  mdegle0  22212  cxple2  22806  rlimcnp3  23025  dchrelbas3  23241  tgcolg  23669  eupath2lem3  24655  isoun  27192  fz0n  28585  onint1  29491  ftc1anclem6  29672  gicabl  30651  dfacbasgrp  30661  sdrgacs  30755  elabrexg  31012  eliooshift  31105  ellimcabssub0  31159  bj-nfcsym  33541  lcvexchlem1  33831  ltrnatb  34933  cdlemg27b  35492