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  695  rspcimdv  3555  riotass2  7347  peano5  7837  oeordi  8516  isf34lem4  10290  domtriomlem  10355  axcclem  10370  ssnn0fi  13938  repswrevw  14740  rlimcn1  15541  climcn1  15545  climcn2  15546  dvdsgcd  16504  lcmfunsnlem2lem1  16598  coprmgcdb  16609  nprm  16648  pcqmul  16815  prmgaplem7  17019  lubun  18472  grpid  18942  psgnunilem4  19463  gexdvds  19550  rngqiprngfulem2  21302  rngqipring1  21306  scmate  22485  cayleyhamilton1  22867  uniopn  22872  tgcmp  23376  uncmp  23378  nconnsubb  23398  comppfsc  23507  kgencn2  23532  isufil2  23883  cfinufil  23903  fin1aufil  23907  flimopn  23950  cnpflf  23976  flimfnfcls  24003  fcfnei  24010  metcnp3  24515  cncfco  24884  ellimc3  25856  dvfsumrlim  26008  cxploglim  26955  2sqreultblem  27425  nbuhgr2vtx1edgblem  29434  nbusgrvtxm1  29462  wlkp1lem6  29760  pthdlem2lem  29850  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  wlknwwlksnbij  29971  eupth2  30324  frgrncvvdeqlem8  30391  grpoid  30606  blocnilem  30890  htthlem  31003  nmcexi  32112  dmdbr3  32391  dmdbr4  32392  atom1d  32439  dvelimalcased  35233  dvelimexcased  35235  mclsax  35767  dfon2lem8  35986  nn0prpwlem  36520  bj-ceqsalt0  37207  bj-ceqsalt1  37208  filbcmb  38075  divrngidl  38363  lshpcmp  39448  lsat0cv  39493  atnle  39777  lpolconN  41947  ss2iundf  44104  iccpartdisj  47909  lighneallem2  48081  lighneallem3  48082  lighneallem4  48085  proththd  48089  sgoldbeven3prm  48271  bgoldbtbndlem2  48294  upgrimwlklem5  48389  upgrwlkupwlk  48628  lindslinindsimp1  48945  nn0sumshdiglemA  49107  eenglngeehlnmlem2  49226  setrec1lem4  50177