MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2thd Structured version   Unicode version

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
StepHypRef Expression
1 2thd.1 . 2  |-  ( ph  ->  ps )
2 2thd.2 . 2  |-  ( ph  ->  ch )
3 pm5.1im 238 . 2  |-  ( ps 
->  ( ch  ->  ( ps 
<->  ch ) ) )
41, 2, 3sylc 60 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator