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

Theorem 2thd 240
Description: Two truths are equivalent (deduction rule). (Contributed by NM, 3-Jun-2012.)
Hypotheses
Ref Expression
2thd.1
2thd.2
Assertion
Ref Expression
2thd

Proof of Theorem 2thd
StepHypRef Expression
1 2thd.1 . 2
2 2thd.2 . 2
3 pm5.1im 238 . 2
41, 2, 3sylc 60 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  had1  1470  sbc2or  3336  abvor0  3803  ralidm  3933  disjprg  4448  euotd  4753  posn  5073  frsn  5075  cnvpo  5550  elabrex  6155  riota5f  6282  smoord  7055  brwdom2  8020  finacn  8452  acacni  8541  dfac13  8543  fin1a2lem10  8810  gch2  9074  gchac  9080  recmulnq  9363  nn1m1nn  10581  nn0sub  10871  qextltlem  11430  xsubge0  11482  xlesubadd  11484  iccshftr  11683  iccshftl  11685  iccdil  11687  icccntr  11689  fzaddel  11747  elfzomelpfzo  11914  sqlecan  12274  nnesq  12290  hashdom  12447  swrdspsleq  12673  repswsymballbi  12752  znnenlem  13945  bitsmod  14086  dvdssq  14198  pcdvdsb  14392  vdwmc2  14497  acsfn  15056  subsubc  15222  funcres2b  15266  isipodrs  15791  issubg3  16219  opnnei  19621  lmss  19799  lmres  19801  cmpfi  19908  xkopt  20156  acufl  20418  lmhmclm  21586  equivcmet  21754  degltlem1  22472  mdegle0  22477  cxple2  23078  rlimcnp3  23297  dchrelbas3  23513  tgcolg  23941  hlbtwn  23995  eupath2lem3  24979  isoun  27520  msrrcl  28903  fz0n  29110  onint1  29914  ftc1anclem6  30095  gicabl  31047  dfacbasgrp  31057  sdrgacs  31150  radcnvrat  31195  elabrexg  31430  eliooshift  31541  ellimcabssub0  31623  bj-nfcsym  34460  lcvexchlem1  34759  ltrnatb  35861  cdlemg27b  36422  rp-fakeimass  37736
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
  Copyright terms: Public domain W3C validator