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

Theorem 2thd 257
Description: Two truths are equivalent. Deduction form. (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 255 . 2 (𝜓 → (𝜒 → (𝜓𝜒)))
41, 2, 3sylc 65 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198
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 199
This theorem is referenced by:  sbc2or  3642  ralidm  4268  disjprg  4839  euotd  5169  posn  5392  frsn  5394  cnvpo  5892  elabrex  6729  riota5f  6864  smoord  7701  brwdom2  8720  finacn  9159  acacni  9250  dfac13  9252  fin1a2lem10  9519  gch2  9785  gchac  9791  recmulnq  10074  nn1m1nn  11334  nn0sub  11632  xnn0n0n1ge2b  12212  qextltlem  12282  xsubge0  12340  xlesubadd  12342  iccshftr  12560  iccshftl  12562  iccdil  12564  icccntr  12566  fzaddel  12629  elfzomelpfzo  12827  sqlecan  13225  nnesq  13242  hashdom  13418  swrdspsleq  13703  repswsymballbi  13860  znnenlemOLD  15276  m1exp1  15429  bitsmod  15493  dvdssq  15615  pcdvdsb  15906  vdwmc2  16016  acsfn  16634  subsubc  16827  funcres2b  16871  isipodrs  17476  issubg3  17925  opnnei  21253  lmss  21431  lmres  21433  cmpfi  21540  xkopt  21787  acufl  22049  lmhmclm  23214  equivcmet  23443  degltlem1  24173  mdegle0  24178  cxple2  24784  rlimcnp3  25046  dchrelbas3  25315  tgcolg  25805  hlbtwn  25862  eupth2lem3lem6  27578  isoun  29997  smatrcl  30378  msrrcl  31957  fz0n  32130  onint1  32956  bj-nfcsym  33377  matunitlindf  33896  ftc1anclem6  33978  lcvexchlem1  35055  ltrnatb  36158  cdlemg27b  36717  gicabl  38454  dfacbasgrp  38463  sdrgacs  38556  rp-fakeimass  38641  or3or  39101  radcnvrat  39295  elabrexg  39966  eliooshift  40477  ellimcabssub0  40593
  Copyright terms: Public domain W3C validator