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  3569  riotass2  7404  peano5  7894  oeordi  8579  isf34lem4  10383  domtriomlem  10448  axcclem  10463  ssnn0fi  14053  repswrevw  14862  rlimcn1  15679  climcn1  15683  climcn2  15684  dvdsgcd  16640  lcmfunsnlem2lem1  16734  coprmgcdb  16745  nprm  16784  pcqmul  16951  prmgaplem7  17155  lubun  18609  grpid  19105  psgnunilem4  19630  gexdvds  19717  rngqiprngfulem2  21521  rngqipring1  21525  scmate  22738  cayleyhamilton1  23123  uniopn  23128  tgcmp  23632  uncmp  23634  nconnsubb  23654  comppfsc  23764  kgencn2  23789  isufil2  24140  cfinufil  24160  fin1aufil  24164  flimopn  24207  cnpflf  24233  flimfnfcls  24260  fcfnei  24267  metcnp3  24772  cncfco  25141  ellimc3  26113  dvfsumrlim  26265  cxploglim  27222  2sqreultblem  27692  nbuhgr2vtx1edgblem  29819  nbusgrvtxm1  29847  wlkp1lem6  30144  pthdlem2lem  30240  crctcshwlkn0lem4  30289  crctcshwlkn0lem5  30290  wlknwwlksnbij  30364  eupth2  30727  frgrncvvdeqlem8  30794  grpoid  31009  blocnilem  31293  htthlem  31406  nmcexi  32515  dmdbr3  32794  dmdbr4  32795  atom1d  32842  dvelimalcased  35592  dvelimexcased  35594  mclsax  36156  dfon2lem8  36375  nn0prpwlem  36949  bj-ceqsalt0  37635  bj-ceqsalt1  37636  filbcmb  38498  divrngidl  38786  lshpcmp  39869  lsat0cv  39914  atnle  40198  lpolconN  42368  ss2iundf  44507  iccpartdisj  48345  lighneallem2  48517  lighneallem3  48518  lighneallem4  48521  proththd  48525  sgoldbeven3prm  48707  bgoldbtbndlem2  48730  upgrimwlklem5  48825  upgrwlkupwlk  49064  lindslinindsimp1  49395  nn0sumshdiglemA  49557  eenglngeehlnmlem2  49676  setrec1lem4  50624  nellindf  50811