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

Theorem 2thd 255
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 253 . 2 (𝜓 → (𝜒 → (𝜓𝜒)))
41, 2, 3sylc 65 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  sbc2or  3594  ralidm  4214  disjprg  4780  euotd  5106  posn  5327  frsn  5329  cnvpo  5817  elabrex  6643  riota5f  6778  smoord  7614  brwdom2  8633  finacn  9072  acacni  9163  dfac13  9165  fin1a2lem10  9432  gch2  9698  gchac  9704  recmulnq  9987  nn1m1nn  11241  nn0sub  11544  xnn0n0n1ge2b  12169  qextltlem  12237  xsubge0  12295  xlesubadd  12297  iccshftr  12512  iccshftl  12514  iccdil  12516  icccntr  12518  fzaddel  12581  elfzomelpfzo  12779  sqlecan  13177  nnesq  13194  hashdom  13369  swrdspsleq  13657  repswsymballbi  13735  znnenlem  15145  m1exp1  15300  bitsmod  15365  dvdssq  15487  pcdvdsb  15779  vdwmc2  15889  acsfn  16526  subsubc  16719  funcres2b  16763  isipodrs  17368  issubg3  17819  opnnei  21144  lmss  21322  lmres  21324  cmpfi  21431  xkopt  21678  acufl  21940  lmhmclm  23105  equivcmet  23332  degltlem1  24051  mdegle0  24056  cxple2  24663  rlimcnp3  24914  dchrelbas3  25183  tgcolg  25669  hlbtwn  25726  eupth2lem3lem6  27410  isoun  29813  smatrcl  30196  msrrcl  31772  fz0n  31948  onint1  32779  bj-nfcsym  33209  matunitlindf  33733  ftc1anclem6  33815  lcvexchlem1  34836  ltrnatb  35938  cdlemg27b  36498  gicabl  38188  dfacbasgrp  38197  sdrgacs  38290  rp-fakeimass  38376  or3or  38838  radcnvrat  39032  elabrexg  39722  eliooshift  40244  ellimcabssub0  40361
  Copyright terms: Public domain W3C validator