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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mp2d  50  pm2.43a  55  embantd  60  mpan2d  707  rspcimdv  3567  riotass2  7399  peano5  7894  oeordi  8580  setrec1lem4  9952  isf34lem4  10436  domtriomlem  10501  axcclem  10516  ssnn0fi  14108  repswrevw  14918  rlimcn1  15735  climcn1  15739  climcn2  15740  dvdsgcd  16697  lcmfunsnlem2lem1  16793  coprmgcdb  16804  nprm  16843  pcqmul  17011  prmgaplem7  17215  lubun  18669  grpid  19166  psgnunilem4  19691  gexdvds  19778  rngqiprngfulem2  21588  rngqipring1  21592  scmate  22805  cayleyhamilton1  23190  uniopn  23195  tgcmp  23699  uncmp  23701  nconnsubb  23721  comppfsc  23831  kgencn2  23856  isufil2  24207  cfinufil  24227  fin1aufil  24231  flimopn  24274  cnpflf  24300  flimfnfcls  24327  fcfnei  24334  metcnp3  24839  cncfco  25208  ellimc3  26179  dvfsumrlim  26331  cxploglim  27287  2sqreultblem  27757  nbuhgr2vtx1edgblem  29914  nbusgrvtxm1  29942  wlkp1lem6  30239  pthdlem2lem  30335  crctcshwlkn0lem4  30384  crctcshwlkn0lem5  30385  wlknwwlksnbij  30459  eupth2  30822  frgrncvvdeqlem8  30889  grpoid  31104  blocnilem  31388  htthlem  31501  nmcexi  32610  dmdbr3  32889  dmdbr4  32890  atom1d  32937  dvelimalcased  35688  dvelimexcased  35690  mclsax  36303  dfon2lem8  36522  nn0prpwlem  37080  bj-ceqsalt0  37766  bj-ceqsalt1  37767  filbcmb  38642  divrngidl  38930  lshpcmp  40013  lsat0cv  40058  atnle  40342  lpolconN  42512  ss2iundf  44618  iccpartdisj  48463  lighneallem2  48635  lighneallem3  48636  lighneallem4  48639  proththd  48643  sgoldbeven3prm  48825  bgoldbtbndlem2  48848  upgrimwlklem5  48943  upgrwlkupwlk  49182  lindslinindsimp1  49513  nn0sumshdiglemA  49675  eenglngeehlnmlem2  49794  nellindf  50914