Theorem 2thd 243

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 241	. 2 |- ( ps -> ( ch -> ( ps <-> ch ) ) )
4	1, 2, 3	sylc 62	1 |- ( ph -> ( ps <-> ch ) )

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

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 188

This theorem is referenced by:  sbc2or  3314  abvor0  3786  ralidm  3907  disjprg  4422  euotd  4722  posn  4923  frsn  4925  cnvpo  5394  elabrex  6163  riota5f  6291  smoord  7092  brwdom2  8088  finacn  8479  acacni  8568  dfac13  8570  fin1a2lem10  8837  gch2  9099  gchac  9105  recmulnq  9388  nn1m1nn  10629  nn0sub  10920  qextltlem  11495  xsubge0  11547  xlesubadd  11549  iccshftr  11764  iccshftl  11766  iccdil  11768  icccntr  11770  fzaddel  11831  elfzomelpfzo  12010  sqlecan  12378  nnesq  12393  hashdom  12555  swrdspsleq  12790  repswsymballbi  12868  znnenlem  14242  bitsmod  14384  dvdssq  14499  pcdvdsb  14781  vdwmc2  14892  acsfn  15516  subsubc  15709  funcres2b  15753  isipodrs  16358  issubg3  16786  opnnei  20067  lmss  20245  lmres  20247  cmpfi  20354  xkopt  20601  acufl  20863  lmhmclm  22010  equivcmet  22178  degltlem1  22898  mdegle0  22903  cxple2  23507  rlimcnp3  23758  dchrelbas3  24029  tgcolg  24459  hlbtwn  24516  eupath2lem3  25552  isoun  28122  smatrcl  28461  msrrcl  29969  fz0n  30151  onint1  30894  bj-nfcsym  31244  ftc1anclem6  31726  lcvexchlem1  32309  ltrnatb  33411  cdlemg27b  33972  gicabl  35663  dfacbasgrp  35673  sdrgacs  35766  rp-fakeimass  35855  radcnvrat  36300  elabrexg  37010  eliooshift  37189  ellimcabssub0  37269