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  1474  sbc2or  3333  abvor0  3802  ralidm  3921  disjprg  4435  euotd  4737  posn  5057  frsn  5059  cnvpo  5528  elabrex  6130  riota5f  6256  smoord  7028  brwdom2  7991  finacn  8422  acacni  8511  dfac13  8513  fin1a2lem10  8780  gch2  9042  gchac  9048  recmulnq  9331  nn1m1nn  10551  nn0sub  10842  qextltlem  11404  xsubge0  11456  xlesubadd  11458  iccshftr  11657  iccshftl  11659  iccdil  11661  icccntr  11663  fzaddel  11722  elfzomelpfzo  11895  sqlecan  12256  nnesq  12272  hashdom  12430  swrdspsleq  12665  repswsymballbi  12743  znnenlem  14029  bitsmod  14170  dvdssq  14282  pcdvdsb  14476  vdwmc2  14581  acsfn  15148  subsubc  15341  funcres2b  15385  isipodrs  15990  issubg3  16418  opnnei  19788  lmss  19966  lmres  19968  cmpfi  20075  xkopt  20322  acufl  20584  lmhmclm  21752  equivcmet  21920  degltlem1  22638  mdegle0  22643  cxple2  23246  rlimcnp3  23495  dchrelbas3  23711  tgcolg  24142  hlbtwn  24196  eupath2lem3  25181  isoun  27748  msrrcl  29167  fz0n  29351  onint1  30142  ftc1anclem6  30335  gicabl  31288  dfacbasgrp  31298  sdrgacs  31391  radcnvrat  31436  elabrexg  31670  eliooshift  31780  ellimcabssub0  31862  bj-nfcsym  34861  lcvexchlem1  35156  ltrnatb  36258  cdlemg27b  36819  rp-fakeimass  38150