Theorem 2thd 244

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

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

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 189

This theorem is referenced by:  sbc2or  3275  abvor0  3749  ralidm  3872  disjprg  4397  euotd  4701  posn  4902  frsn  4904  cnvpo  5373  elabrex  6146  riota5f  6274  smoord  7081  brwdom2  8085  finacn  8478  acacni  8567  dfac13  8569  fin1a2lem10  8836  gch2  9097  gchac  9103  recmulnq  9386  nn1m1nn  10626  nn0sub  10917  qextltlem  11492  xsubge0  11544  xlesubadd  11546  iccshftr  11763  iccshftl  11765  iccdil  11767  icccntr  11769  fzaddel  11830  elfzomelpfzo  12010  sqlecan  12378  nnesq  12393  hashdom  12555  swrdspsleq  12800  repswsymballbi  12878  znnenlem  14257  bitsmod  14403  dvdssq  14521  pcdvdsb  14811  vdwmc2  14922  acsfn  15558  subsubc  15751  funcres2b  15795  isipodrs  16400  issubg3  16828  opnnei  20129  lmss  20307  lmres  20309  cmpfi  20416  xkopt  20663  acufl  20925  lmhmclm  22110  equivcmet  22278  degltlem1  23014  mdegle0  23019  cxple2  23635  rlimcnp3  23886  dchrelbas3  24159  tgcolg  24592  hlbtwn  24649  eupath2lem3  25700  isoun  28275  smatrcl  28615  msrrcl  30174  fz0n  30357  onint1  31102  bj-nfcsym  31487  ftc1anclem6  32015  lcvexchlem1  32594  ltrnatb  33696  cdlemg27b  34257  gicabl  35951  dfacbasgrp  35961  sdrgacs  36061  rp-fakeimass  36150  radcnvrat  36657  elabrexg  37364  eliooshift  37598  ellimcabssub0  37691