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

Theorem mpid 42
Description: A nested modus ponens deduction. Deduction associated with mpi 20. (Contributed by NM, 14-Dec-2004.)
Hypotheses
Ref Expression
mpid.1  |-  ( ph  ->  ch )
mpid.2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
mpid  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem mpid
StepHypRef Expression
1 mpid.1 . . 3  |-  ( ph  ->  ch )
21a1d 26 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 mpid.2 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpdd 41 1  |-  ( ph  ->  ( ps  ->  th )
)
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  46  pm2.43a  51  embantd  56  mtord  670  mpan2d  685  ceqsalt  3082  rspcimdv  3163  riotass2  6303  peano5  6743  oeordi  7314  isf34lem4  8833  domtriomlem  8898  axcclem  8913  ssnn0fi  12229  repswrevw  12926  rlimcn1  13701  climcn1  13704  climcn2  13705  dvdsgcd  14560  lcmfunsnlem2lem1  14660  nprm  14687  coprmgcdb  14703  pcqmul  14852  prmgaplem7  15076  lubun  16418  grpid  16750  psgnunilem4  17187  gexdvds  17284  scmate  19584  cayleyhamilton1  19965  uniopn  19976  tgcmp  20465  uncmp  20467  nconsubb  20487  comppfsc  20596  kgencn2  20621  isufil2  20972  cfinufil  20992  fin1aufil  20996  flimopn  21039  cnpflf  21065  flimfnfcls  21092  fcfnei  21099  metcnp3  21604  cncfco  21988  ellimc3  22883  dvfsumrlim  23032  cxploglim  23952  constr3trllem2  25428  frgrancvvdeqlemB  25815  grpoid  26000  blocnilem  26494  htthlem  26619  nmcexi  27728  dmdbr3  28007  dmdbr4  28008  atom1d  28055  mclsax  30256  dfon2lem8  30485  nn0prpwlem  31027  nn0prpw  31028  bj-ceqsalt0  31527  bj-ceqsalt1  31528  filbcmb  32112  divrngidl  32306  lshpcmp  32599  lsat0cv  32644  atnle  32928  lpolconN  35100  ss2iundf  36296  iccpartgt  38779  iccpartdisj  38789  bgoldbtbndlem2  38939  proththd  38952  nbuhgr2vtx1edgblem  39469  nbusgrvtxm1  39503  upgr1wlkwlk  39700  pthdlem2lem  39793  lindslinindsimp1  40523  nn0sumshdiglemA  40703
  Copyright terms: Public domain W3C validator