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  3474  rspcimdv  3570  riotass2  7345  peano5  7831  peano5OLD  7832  oeordi  8535  isf34lem4  10318  domtriomlem  10383  axcclem  10398  ssnn0fi  13896  repswrevw  14681  rlimcn1  15476  climcn1  15480  climcn2  15481  dvdsgcd  16430  lcmfunsnlem2lem1  16519  coprmgcdb  16530  nprm  16569  pcqmul  16730  prmgaplem7  16934  lubun  18409  grpid  18791  psgnunilem4  19284  gexdvds  19371  scmate  21875  cayleyhamilton1  22257  uniopn  22262  tgcmp  22768  uncmp  22770  nconnsubb  22790  comppfsc  22899  kgencn2  22924  isufil2  23275  cfinufil  23295  fin1aufil  23299  flimopn  23342  cnpflf  23368  flimfnfcls  23395  fcfnei  23402  metcnp3  23912  cncfco  24286  ellimc3  25259  dvfsumrlim  25411  cxploglim  26343  2sqreultblem  26812  nbuhgr2vtx1edgblem  28341  nbusgrvtxm1  28369  wlkp1lem6  28668  pthdlem2lem  28757  crctcshwlkn0lem4  28800  crctcshwlkn0lem5  28801  wlknwwlksnbij  28875  eupth2  29225  frgrncvvdeqlem8  29292  grpoid  29504  blocnilem  29788  htthlem  29901  nmcexi  31010  dmdbr3  31289  dmdbr4  31290  atom1d  31337  mclsax  34220  dfon2lem8  34421  nn0prpwlem  34840  bj-ceqsalt0  35397  bj-ceqsalt1  35398  filbcmb  36245  divrngidl  36533  lshpcmp  37496  lsat0cv  37541  atnle  37825  lpolconN  39996  ss2iundf  42019  iccpartdisj  45715  lighneallem2  45884  lighneallem3  45885  lighneallem4  45888  proththd  45892  sgoldbeven3prm  46061  bgoldbtbndlem2  46084  upgrwlkupwlk  46128  lindslinindsimp1  46624  nn0sumshdiglemA  46791  eenglngeehlnmlem2  46910  setrec1lem4  47221
  Copyright terms: Public domain W3C validator