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  1445  sbc2or  3297  abvor0  3758  ralidm  3886  disjprg  4391  euotd  4695  posn  5010  frsn  5012  cnvpo  5478  elabrex  6064  riota5f  6181  smoord  6931  brwdom2  7894  finacn  8326  acacni  8415  dfac13  8417  fin1a2lem10  8684  gch2  8948  gchac  8954  recmulnq  9239  nn1m1nn  10448  nn0sub  10736  qextltlem  11278  xsubge0  11330  xlesubadd  11332  iccshftr  11531  iccshftl  11533  iccdil  11535  icccntr  11537  fzaddel  11605  elfzomelpfzo  11741  sqlecan  12084  nnesq  12100  hashdom  12255  swrdspsleq  12455  repswsymballbi  12531  znnenlem  13607  bitsmod  13745  dvdssq  13857  pcdvdsb  14048  vdwmc2  14153  acsfn  14711  subsubc  14877  funcres2b  14921  isipodrs  15445  issubg3  15813  opnnei  18851  lmss  19029  lmres  19031  cmpfi  19138  xkopt  19355  acufl  19617  lmhmclm  20785  equivcmet  20953  degltlem1  21671  mdegle0  21676  cxple2  22270  rlimcnp3  22489  dchrelbas3  22705  tgcolg  23119  eupath2lem3  23747  isoun  26143  fz0n  27528  onint1  28434  ftc1anclem6  28615  gicabl  29597  dfacbasgrp  29607  sdrgacs  29701  bj-nfcsym  32708  lcvexchlem1  32998  ltrnatb  34100  cdlemg27b  34659