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

Theorem 2thd 266
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 264 . 2 (𝜓 → (𝜒 → (𝜓𝜒)))
41, 2, 3sylc 65 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  biort  929  vtocl2d  3558  vtocl2  3562  vtocl3  3564  rspcime  3626  sbc2or  3780  ralidm  4453  disjprgw  5053  disjprg  5054  euotd  5395  posn  5631  frsn  5633  cnvpo  6132  elabrex  6993  riota5f  7131  smoord  7993  brwdom2  9026  finacn  9465  acacni  9555  dfac13  9557  fin1a2lem10  9820  gch2  10086  gchac  10092  recmulnq  10375  nn1m1nn  11647  nn0sub  11936  xnn0n0n1ge2b  12516  qextltlem  12585  xnn0lem1lt  12627  xsubge0  12644  xlesubadd  12646  iccshftr  12862  iccshftl  12864  iccdil  12866  icccntr  12868  fzaddel  12931  elfzomelpfzo  13131  sqlecan  13561  nnesq  13578  hashdom  13730  swrdspsleq  14017  repswsymballbi  14132  m1exp1  15717  bitsmod  15775  dvdssq  15901  pcdvdsb  16195  vdwmc2  16305  acsfn  16920  subsubc  17113  funcres2b  17157  isipodrs  17761  issubg3  18237  sdrgacs  19511  opnnei  21658  lmss  21836  lmres  21838  cmpfi  21946  xkopt  22193  acufl  22455  lmhmclm  23620  equivcmet  23849  degltlem1  24595  mdegle0  24600  cxple2  25207  rlimcnp3  25473  dchrelbas3  25742  tgcolg  26268  hlbtwn  26325  eupth2lem3lem6  27940  isoun  30364  smatrcl  30961  msrrcl  32688  fz0n  32860  onint1  33695  bj-animbi  33792  bj-nfcsym  34113  matunitlindf  34772  ftc1anclem6  34854  lcvexchlem1  36052  ltrnatb  37155  cdlemg27b  37714  lmhmlvec  39028  gicabl  39579  dfacbasgrp  39588  rp-fakeimass  39758  or3or  40251  radcnvrat  40526  elabrexg  41183  eliooshift  41662  ellimcabssub0  41778
  Copyright terms: Public domain W3C validator