Theorem mpid 45

Description: A nested modus ponens deduction. Deduction associated with mpi 21. (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 26	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		mpid.2	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	2, 3	mpdd 44	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  50  pm2.43a  55  embantd  60  mpan2d  706  rspcimdv  3572  riotass2  7399  peano5  7891  oeordi  8574  isf34lem4  10362  domtriomlem  10427  axcclem  10442  ssnn0fi  14023  repswrevw  14826  rlimcn1  15641  climcn1  15645  climcn2  15646  dvdsgcd  16603  lcmfunsnlem2lem1  16697  coprmgcdb  16708  nprm  16747  pcqmul  16914  prmgaplem7  17118  lubun  18572  grpid  19043  psgnunilem4  19568  gexdvds  19655  rngqiprngfulem2  21433  rngqipring1  21437  scmate  22648  cayleyhamilton1  23030  uniopn  23035  tgcmp  23539  uncmp  23541  nconnsubb  23561  comppfsc  23670  kgencn2  23695  isufil2  24046  cfinufil  24066  fin1aufil  24070  flimopn  24113  cnpflf  24139  flimfnfcls  24166  fcfnei  24173  metcnp3  24678  cncfco  25047  ellimc3  26019  dvfsumrlim  26171  cxploglim  27120  2sqreultblem  27590  nbuhgr2vtx1edgblem  29679  nbusgrvtxm1  29707  wlkp1lem6  30004  pthdlem2lem  30094  crctcshwlkn0lem4  30140  crctcshwlkn0lem5  30141  wlknwwlksnbij  30215  eupth2  30568  frgrncvvdeqlem8  30635  grpoid  30850  blocnilem  31134  htthlem  31247  nmcexi  32356  dmdbr3  32635  dmdbr4  32636  atom1d  32683  dvelimalcased  35441  dvelimexcased  35443  mclsax  36039  dfon2lem8  36258  nn0prpwlem  36811  bj-ceqsalt0  37497  bj-ceqsalt1  37498  filbcmb  38369  divrngidl  38657  lshpcmp  39740  lsat0cv  39785  atnle  40069  lpolconN  42239  ss2iundf  44365  iccpartdisj  48163  lighneallem2  48335  lighneallem3  48336  lighneallem4  48339  proththd  48343  sgoldbeven3prm  48525  bgoldbtbndlem2  48548  upgrimwlklem5  48643  upgrwlkupwlk  48882  lindslinindsimp1  49214  nn0sumshdiglemA  49376  eenglngeehlnmlem2  49495  setrec1lem4  50445