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  1457  sbc2or  3322  abvor0  3789  ralidm  3918  disjprg  4433  euotd  4738  posn  5058  frsn  5060  cnvpo  5535  elabrex  6140  riota5f  6267  smoord  7038  brwdom2  8002  finacn  8434  acacni  8523  dfac13  8525  fin1a2lem10  8792  gch2  9056  gchac  9062  recmulnq  9345  nn1m1nn  10562  nn0sub  10852  qextltlem  11410  xsubge0  11462  xlesubadd  11464  iccshftr  11663  iccshftl  11665  iccdil  11667  icccntr  11669  fzaddel  11727  elfzomelpfzo  11893  sqlecan  12253  nnesq  12269  hashdom  12426  swrdspsleq  12652  repswsymballbi  12731  znnenlem  13822  bitsmod  13963  dvdssq  14075  pcdvdsb  14269  vdwmc2  14374  acsfn  14933  subsubc  15096  funcres2b  15140  isipodrs  15665  issubg3  16093  opnnei  19494  lmss  19672  lmres  19674  cmpfi  19781  xkopt  20029  acufl  20291  lmhmclm  21459  equivcmet  21627  degltlem1  22345  mdegle0  22350  cxple2  22950  rlimcnp3  23169  dchrelbas3  23385  tgcolg  23813  hlbtwn  23867  eupath2lem3  24851  isoun  27392  msrrcl  28776  fz0n  28983  onint1  29889  ftc1anclem6  30070  gicabl  31022  dfacbasgrp  31032  sdrgacs  31126  radcnvrat  31171  elabrexg  31384  eliooshift  31477  ellimcabssub0  31531  bj-nfcsym  34208  lcvexchlem1  34499  ltrnatb  35601  cdlemg27b  36162  rp-fakeimass  37439