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

Theorem mpid 44
Description: A nested modus ponens deduction. Deduction associated with mpi 20. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
mpid.1 (𝜑𝜒)
mpid.2 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
mpid (𝜑 → (𝜓𝜃))

Proof of Theorem mpid
StepHypRef Expression
1 mpid.1 . . 3 (𝜑𝜒)
21a1d 25 . 2 (𝜑 → (𝜓𝜒))
3 mpid.2 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
42, 3mpdd 43 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mp2d  49  pm2.43a  54  embantd  59  mpan2d  693  ceqsalt  3513  rspcimdv  3599  riotass2  7137  peano5  7599  oeordi  8209  isf34lem4  9797  domtriomlem  9862  axcclem  9877  ssnn0fi  13357  repswrevw  14149  rlimcn1  14945  climcn1  14948  climcn2  14949  dvdsgcd  15890  lcmfunsnlem2lem1  15980  coprmgcdb  15991  nprm  16030  pcqmul  16188  prmgaplem7  16391  lubun  17733  grpid  18139  psgnunilem4  18625  gexdvds  18709  scmate  21122  cayleyhamilton1  21504  uniopn  21509  tgcmp  22013  uncmp  22015  nconnsubb  22035  comppfsc  22144  kgencn2  22169  isufil2  22520  cfinufil  22540  fin1aufil  22544  flimopn  22587  cnpflf  22613  flimfnfcls  22640  fcfnei  22647  metcnp3  23154  cncfco  23519  ellimc3  24489  dvfsumrlim  24641  cxploglim  25570  2sqreultblem  26039  nbuhgr2vtx1edgblem  27148  nbusgrvtxm1  27176  wlkp1lem6  27475  pthdlem2lem  27563  crctcshwlkn0lem4  27606  crctcshwlkn0lem5  27607  wlknwwlksnbij  27681  eupth2  28031  frgrncvvdeqlem8  28098  grpoid  28310  blocnilem  28594  htthlem  28707  nmcexi  29816  dmdbr3  30095  dmdbr4  30096  atom1d  30143  mclsax  32877  dfon2lem8  33096  nn0prpwlem  33731  bj-ceqsalt0  34272  bj-ceqsalt1  34273  filbcmb  35127  divrngidl  35415  lshpcmp  36233  lsat0cv  36278  atnle  36562  lpolconN  38732  ss2iundf  40281  iccpartdisj  43885  lighneallem2  44055  lighneallem3  44056  lighneallem4  44059  proththd  44063  sgoldbeven3prm  44232  bgoldbtbndlem2  44255  upgrwlkupwlk  44299  lindslinindsimp1  44797  nn0sumshdiglemA  44964  eenglngeehlnmlem2  45083  setrec1lem4  45151
  Copyright terms: Public domain W3C validator