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  931  vtocl2d  3563  vtocl2  3567  vtocl3  3569  rspcime  3631  sbc2or  3785  ralidm  4458  disjprgw  5058  disjprg  5059  euotd  5400  posn  5636  frsn  5638  cnvpo  6137  elabrex  6998  riota5f  7136  smoord  7998  brwdom2  9031  finacn  9470  acacni  9560  dfac13  9562  fin1a2lem10  9825  gch2  10091  gchac  10097  recmulnq  10380  nn1m1nn  11652  nn0sub  11941  xnn0n0n1ge2b  12521  qextltlem  12590  xnn0lem1lt  12632  xsubge0  12649  xlesubadd  12651  iccshftr  12867  iccshftl  12869  iccdil  12871  icccntr  12873  fzaddel  12936  elfzomelpfzo  13136  sqlecan  13566  nnesq  13583  hashdom  13735  swrdspsleq  14022  repswsymballbi  14137  m1exp1  15722  bitsmod  15780  dvdssq  15906  pcdvdsb  16200  vdwmc2  16310  acsfn  16925  subsubc  17118  funcres2b  17162  isipodrs  17766  issubg3  18242  sdrgacs  19516  opnnei  21663  lmss  21841  lmres  21843  cmpfi  21951  xkopt  22198  acufl  22460  lmhmclm  23625  equivcmet  23854  degltlem1  24600  mdegle0  24605  cxple2  25212  rlimcnp3  25478  dchrelbas3  25747  tgcolg  26273  hlbtwn  26330  eupth2lem3lem6  27945  isoun  30369  smatrcl  30966  msrrcl  32693  fz0n  32865  onint1  33700  bj-animbi  33797  bj-nfcsym  34118  matunitlindf  34776  ftc1anclem6  34858  lcvexchlem1  36056  ltrnatb  37159  cdlemg27b  37718  lmhmlvec  39032  gicabl  39583  dfacbasgrp  39592  rp-fakeimass  39762  or3or  40255  radcnvrat  40530  elabrexg  41187  eliooshift  41666  ellimcabssub0  41782
 Copyright terms: Public domain W3C validator