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  704  rspcimdv  3571  riotass2  7379  peano5  7870  oeordi  8552  isf34lem4  10331  domtriomlem  10396  axcclem  10411  ssnn0fi  13995  repswrevw  14797  rlimcn1  15598  climcn1  15602  climcn2  15603  dvdsgcd  16561  lcmfunsnlem2lem1  16655  coprmgcdb  16666  nprm  16705  pcqmul  16872  prmgaplem7  17076  lubun  18530  grpid  19000  psgnunilem4  19520  gexdvds  19607  rngqiprngfulem2  21362  rngqipring1  21366  scmate  22550  cayleyhamilton1  22932  uniopn  22937  tgcmp  23441  uncmp  23443  nconnsubb  23463  comppfsc  23572  kgencn2  23597  isufil2  23948  cfinufil  23968  fin1aufil  23972  flimopn  24015  cnpflf  24041  flimfnfcls  24068  fcfnei  24075  metcnp3  24580  cncfco  24949  ellimc3  25921  dvfsumrlim  26073  cxploglim  27019  2sqreultblem  27489  nbuhgr2vtx1edgblem  29498  nbusgrvtxm1  29526  wlkp1lem6  29823  pthdlem2lem  29913  crctcshwlkn0lem4  29959  crctcshwlkn0lem5  29960  wlknwwlksnbij  30034  eupth2  30387  frgrncvvdeqlem8  30454  grpoid  30669  blocnilem  30953  htthlem  31066  nmcexi  32175  dmdbr3  32454  dmdbr4  32455  atom1d  32502  dvelimalcased  35334  dvelimexcased  35336  mclsax  35883  dfon2lem8  36102  nn0prpwlem  36646  bj-ceqsalt0  37333  bj-ceqsalt1  37334  filbcmb  38203  divrngidl  38491  lshpcmp  39576  lsat0cv  39621  atnle  39905  lpolconN  42075  ss2iundf  44199  iccpartdisj  48007  lighneallem2  48179  lighneallem3  48180  lighneallem4  48183  proththd  48187  sgoldbeven3prm  48369  bgoldbtbndlem2  48392  upgrimwlklem5  48487  upgrwlkupwlk  48726  lindslinindsimp1  49043  nn0sumshdiglemA  49205  eenglngeehlnmlem2  49324  setrec1lem4  50275