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  3581  riotass2  7377  peano5  7872  oeordi  8554  isf34lem4  10337  domtriomlem  10402  axcclem  10417  ssnn0fi  13957  repswrevw  14759  rlimcn1  15561  climcn1  15565  climcn2  15566  dvdsgcd  16521  lcmfunsnlem2lem1  16615  coprmgcdb  16626  nprm  16665  pcqmul  16831  prmgaplem7  17035  lubun  18481  grpid  18914  psgnunilem4  19434  gexdvds  19521  rngqiprngfulem2  21229  rngqipring1  21233  scmate  22404  cayleyhamilton1  22786  uniopn  22791  tgcmp  23295  uncmp  23297  nconnsubb  23317  comppfsc  23426  kgencn2  23451  isufil2  23802  cfinufil  23822  fin1aufil  23826  flimopn  23869  cnpflf  23895  flimfnfcls  23922  fcfnei  23929  metcnp3  24435  cncfco  24807  ellimc3  25787  dvfsumrlim  25945  cxploglim  26895  2sqreultblem  27366  nbuhgr2vtx1edgblem  29285  nbusgrvtxm1  29313  wlkp1lem6  29613  pthdlem2lem  29704  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  wlknwwlksnbij  29825  eupth2  30175  frgrncvvdeqlem8  30242  grpoid  30456  blocnilem  30740  htthlem  30853  nmcexi  31962  dmdbr3  32241  dmdbr4  32242  atom1d  32289  dvelimalcased  35072  dvelimexcased  35074  mclsax  35563  dfon2lem8  35785  nn0prpwlem  36317  bj-ceqsalt0  36879  bj-ceqsalt1  36880  filbcmb  37741  divrngidl  38029  lshpcmp  38988  lsat0cv  39033  atnle  39317  lpolconN  41488  ss2iundf  43655  iccpartdisj  47442  lighneallem2  47611  lighneallem3  47612  lighneallem4  47615  proththd  47619  sgoldbeven3prm  47788  bgoldbtbndlem2  47811  upgrimwlklem5  47905  upgrwlkupwlk  48132  lindslinindsimp1  48450  nn0sumshdiglemA  48612  eenglngeehlnmlem2  48731  setrec1lem4  49683