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

Theorem mpdd 40
Description: A nested modus ponens deduction. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mpdd.1
mpdd.2
Assertion
Ref Expression
mpdd

Proof of Theorem mpdd
StepHypRef Expression
1 mpdd.1 . 2
2 mpdd.2 . . 3
32a2d 26 . 2
41, 3mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  mpid  41  mpdi  42  syld  44  syl6c  64  mpteqb  5970  oprabid  6323  frxp  6910  smo11  7054  oaordex  7226  oaass  7229  omordi  7234  oeordsuc  7262  nnmordi  7299  nnmord  7300  nnaordex  7306  brecop  7423  findcard2  7780  elfiun  7910  ordiso2  7961  ordtypelem7  7970  cantnf  8133  cantnfOLD  8155  coftr  8674  domtriomlem  8843  prlem936  9446  zindd  10990  supxrun  11536  ccatopth2  12696  cau3lem  13187  climcau  13493  divalglem8  14058  dirtr  15866  frgpnabllem1  16877  dprddisj2  17087  dprddisj2OLD  17088  znrrg  18604  opnnei  19621  restntr  19683  lpcls  19865  comppfsc  20033  ufilmax  20408  ufileu  20420  flimfnfcls  20529  alexsubALTlem4  20550  qustgplem  20619  metrest  21027  caubl  21746  ulmcau  22790  ulmcn  22794  usgranloopv  24378  erclwwlksym  24814  erclwwlktr  24815  erclwwlknsym  24826  erclwwlkntr  24827  sumdmdlem  27337  fundmpss  29196  dfon2lem8  29222  nodenselem7  29447  nodenselem8  29448  ifscgr  29694  btwnconn1lem11  29747  btwnconn2  29752  finminlem  30136  opnrebl2  30139  filbcmb  30231  seqpo  30240  mpt2bi123f  30571  mptbi12f  30575  ac6s6  30580  truniALT  33312  onfrALTlem3  33316  ee223  33420  bnj1280  34076  dia2dimlem12  36802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator