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  3566  riotass2  7345  peano5  7835  oeordi  8515  isf34lem4  10287  domtriomlem  10352  axcclem  10367  ssnn0fi  13908  repswrevw  14710  rlimcn1  15511  climcn1  15515  climcn2  15516  dvdsgcd  16471  lcmfunsnlem2lem1  16565  coprmgcdb  16576  nprm  16615  pcqmul  16781  prmgaplem7  16985  lubun  18438  grpid  18905  psgnunilem4  19426  gexdvds  19513  rngqiprngfulem2  21267  rngqipring1  21271  scmate  22454  cayleyhamilton1  22836  uniopn  22841  tgcmp  23345  uncmp  23347  nconnsubb  23367  comppfsc  23476  kgencn2  23501  isufil2  23852  cfinufil  23872  fin1aufil  23876  flimopn  23919  cnpflf  23945  flimfnfcls  23972  fcfnei  23979  metcnp3  24484  cncfco  24856  ellimc3  25836  dvfsumrlim  25994  cxploglim  26944  2sqreultblem  27415  nbuhgr2vtx1edgblem  29424  nbusgrvtxm1  29452  wlkp1lem6  29750  pthdlem2lem  29840  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  wlknwwlksnbij  29961  eupth2  30314  frgrncvvdeqlem8  30381  grpoid  30595  blocnilem  30879  htthlem  30992  nmcexi  32101  dmdbr3  32380  dmdbr4  32381  atom1d  32428  dvelimalcased  35231  dvelimexcased  35233  mclsax  35763  dfon2lem8  35982  nn0prpwlem  36516  bj-ceqsalt0  37085  bj-ceqsalt1  37086  filbcmb  37937  divrngidl  38225  lshpcmp  39244  lsat0cv  39289  atnle  39573  lpolconN  41743  ss2iundf  43896  iccpartdisj  47679  lighneallem2  47848  lighneallem3  47849  lighneallem4  47852  proththd  47856  sgoldbeven3prm  48025  bgoldbtbndlem2  48048  upgrimwlklem5  48143  upgrwlkupwlk  48382  lindslinindsimp1  48699  nn0sumshdiglemA  48861  eenglngeehlnmlem2  48980  setrec1lem4  49931