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

Theorem mpid 41
Description: A nested modus ponens deduction. (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 40 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  mp2d  45  pm2.43a  49  embantd  54  mtord  660  mpan2d  674  ceqsalt  3132  rspcimdv  3211  riotass2  6284  peano5  6723  oeordi  7255  isf34lem4  8778  domtriomlem  8843  axcclem  8858  ssnn0fi  12094  repswrevw  12758  rlimcn1  13411  climcn1  13414  climcn2  13415  dvdsgcd  14181  nprm  14231  pcqmul  14377  lubun  15753  grpid  16085  psgnunilem4  16522  gexdvds  16604  scmate  19012  cayleyhamilton1  19393  uniopn  19406  tgcmp  19901  uncmp  19903  nconsubb  19924  comppfsc  20033  kgencn2  20058  isufil2  20409  cfinufil  20429  fin1aufil  20433  flimopn  20476  cnpflf  20502  flimfnfcls  20529  fcfnei  20536  metcnp3  21043  cncfco  21411  ellimc3  22283  dvfsumrlim  22432  cxploglim  23307  constr3trllem2  24651  frgrancvvdeqlemB  25038  grpoid  25225  blocnilem  25719  htthlem  25834  nmcexi  26945  dmdbr3  27224  dmdbr4  27225  atom1d  27272  mclsax  28929  dfon2lem8  29222  nn0prpwlem  30140  nn0prpw  30141  filbcmb  30231  divrngidl  30425  lindslinindsimp1  33058  bj-ceqsalt0  34449  bj-ceqsalt1  34450  lshpcmp  34713  lsat0cv  34758  atnle  35042  lpolconN  37214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator