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

Step	Hyp	Ref	Expression
1		mpid.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		mpid.2	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	2, 3	mpdd 43	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  694  rspcimdv  3611  riotass2  7417  peano5  7915  oeordi  8623  isf34lem4  10414  domtriomlem  10479  axcclem  10494  ssnn0fi  14022  repswrevw  14821  rlimcn1  15620  climcn1  15624  climcn2  15625  dvdsgcd  16577  lcmfunsnlem2lem1  16671  coprmgcdb  16682  nprm  16721  pcqmul  16886  prmgaplem7  17090  lubun  18572  grpid  19005  psgnunilem4  19529  gexdvds  19616  rngqiprngfulem2  21339  rngqipring1  21343  scmate  22531  cayleyhamilton1  22913  uniopn  22918  tgcmp  23424  uncmp  23426  nconnsubb  23446  comppfsc  23555  kgencn2  23580  isufil2  23931  cfinufil  23951  fin1aufil  23955  flimopn  23998  cnpflf  24024  flimfnfcls  24051  fcfnei  24058  metcnp3  24568  cncfco  24946  ellimc3  25928  dvfsumrlim  26086  cxploglim  27035  2sqreultblem  27506  nbuhgr2vtx1edgblem  29382  nbusgrvtxm1  29410  wlkp1lem6  29710  pthdlem2lem  29799  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  wlknwwlksnbij  29917  eupth2  30267  frgrncvvdeqlem8  30334  grpoid  30548  blocnilem  30832  htthlem  30945  nmcexi  32054  dmdbr3  32333  dmdbr4  32334  atom1d  32381  dvelimalcased  35067  dvelimexcased  35069  mclsax  35553  dfon2lem8  35771  nn0prpwlem  36304  bj-ceqsalt0  36866  bj-ceqsalt1  36867  filbcmb  37726  divrngidl  38014  lshpcmp  38969  lsat0cv  39014  atnle  39298  lpolconN  41469  ss2iundf  43648  iccpartdisj  47361  lighneallem2  47530  lighneallem3  47531  lighneallem4  47534  proththd  47538  sgoldbeven3prm  47707  bgoldbtbndlem2  47730  upgrwlkupwlk  47983  lindslinindsimp1  48302  nn0sumshdiglemA  48468  eenglngeehlnmlem2  48587  setrec1lem4  48920