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

Theorem 2thd 253
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 251 . 2 (𝜓 → (𝜒 → (𝜓𝜒)))
41, 2, 3sylc 62 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  sbc2or  3410  ralidm  4026  disjprg  4572  euotd  4891  posn  5100  frsn  5102  cnvpo  5576  elabrex  6383  riota5f  6513  smoord  7326  brwdom2  8338  finacn  8733  acacni  8822  dfac13  8824  fin1a2lem10  9091  gch2  9353  gchac  9359  recmulnq  9642  nn1m1nn  10887  nn0sub  11190  qextltlem  11866  xsubge0  11920  xlesubadd  11922  iccshftr  12133  iccshftl  12135  iccdil  12137  icccntr  12139  fzaddel  12201  elfzomelpfzo  12393  sqlecan  12788  nnesq  12805  hashdom  12981  swrdspsleq  13247  repswsymballbi  13324  znnenlem  14725  m1exp1  14877  bitsmod  14942  dvdssq  15064  pcdvdsb  15357  vdwmc2  15467  acsfn  16089  subsubc  16282  funcres2b  16326  isipodrs  16930  issubg3  17381  opnnei  20676  lmss  20854  lmres  20856  cmpfi  20963  xkopt  21210  acufl  21473  lmhmclm  22626  equivcmet  22839  degltlem1  23553  mdegle0  23558  cxple2  24160  rlimcnp3  24411  dchrelbas3  24680  tgcolg  25167  hlbtwn  25224  eupath2lem3  26272  isoun  28668  smatrcl  28996  msrrcl  30500  fz0n  30675  onint1  31424  bj-nfcsym  31875  matunitlindf  32373  ftc1anclem6  32456  lcvexchlem1  33135  ltrnatb  34237  cdlemg27b  34798  gicabl  36483  dfacbasgrp  36493  sdrgacs  36586  rp-fakeimass  36672  or3or  37135  radcnvrat  37331  elabrexg  38025  eliooshift  38373  ellimcabssub0  38481  xnn0n0n1ge2b  40211  eupth2lem3lem6  41396
  Copyright terms: Public domain W3C validator