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  3570  riotass2  7430  peano5  7929  oeordi  8624  setrec1lem4  9998  isf34lem4  10482  domtriomlem  10547  axcclem  10562  ssnn0fi  14155  repswrevw  14966  rlimcn1  15784  climcn1  15788  climcn2  15789  dvdsgcd  16746  lcmfunsnlem2lem1  16842  coprmgcdb  16853  nprm  16892  pcqmul  17060  prmgaplem7  17264  lubun  18718  grpid  19215  psgnunilem4  19741  gexdvds  19828  rngqiprngfulem2  21638  rngqipring1  21642  scmate  22855  cayleyhamilton1  23240  uniopn  23245  tgcmp  23749  uncmp  23751  nconnsubb  23771  comppfsc  23881  kgencn2  23906  isufil2  24257  cfinufil  24277  fin1aufil  24281  flimopn  24324  cnpflf  24350  flimfnfcls  24377  fcfnei  24384  metcnp3  24889  cncfco  25258  ellimc3  26229  dvfsumrlim  26381  cxploglim  27335  2sqreultblem  27805  nbuhgr2vtx1edgblem  29962  nbusgrvtxm1  29990  wlkp1lem6  30287  pthdlem2lem  30383  crctcshwlkn0lem4  30432  crctcshwlkn0lem5  30433  wlknwwlksnbij  30507  eupth2  30870  frgrncvvdeqlem8  30937  grpoid  31152  blocnilem  31436  htthlem  31549  nmcexi  32658  dmdbr3  32937  dmdbr4  32938  atom1d  32985  dvelimalcased  35775  dvelimexcased  35777  mclsax  36501  dfon2lem8  36730  nn0prpwlem  37288  bj-ceqsalt0  37974  bj-ceqsalt1  37975  filbcmb  38866  divrngidl  39154  lshpcmp  40237  lsat0cv  40282  atnle  40566  lpolconN  42736  ss2iundf  44851  iccpartdisj  48724  lighneallem2  48896  lighneallem3  48897  lighneallem4  48900  proththd  48904  sgoldbeven3prm  49086  bgoldbtbndlem2  49109  upgrimwlklem5  49204  upgrwlkupwlk  49443  lindslinindsimp1  49774  nn0sumshdiglemA  49936  eenglngeehlnmlem2  50056  nellindf  51250