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  3574  riotass2  7410  peano5  7899  oeordi  8582  isf34lem4  10379  domtriomlem  10444  axcclem  10459  ssnn0fi  14041  repswrevw  14850  rlimcn1  15665  climcn1  15669  climcn2  15670  dvdsgcd  16627  lcmfunsnlem2lem1  16721  coprmgcdb  16732  nprm  16771  pcqmul  16938  prmgaplem7  17142  lubun  18596  grpid  19073  psgnunilem4  19598  gexdvds  19685  rngqiprngfulem2  21489  rngqipring1  21493  scmate  22704  cayleyhamilton1  23086  uniopn  23091  tgcmp  23595  uncmp  23597  nconnsubb  23617  comppfsc  23726  kgencn2  23751  isufil2  24102  cfinufil  24122  fin1aufil  24126  flimopn  24169  cnpflf  24195  flimfnfcls  24222  fcfnei  24229  metcnp3  24734  cncfco  25103  ellimc3  26075  dvfsumrlim  26227  cxploglim  27179  2sqreultblem  27649  nbuhgr2vtx1edgblem  29738  nbusgrvtxm1  29766  wlkp1lem6  30063  pthdlem2lem  30153  crctcshwlkn0lem4  30199  crctcshwlkn0lem5  30200  wlknwwlksnbij  30274  eupth2  30627  frgrncvvdeqlem8  30694  grpoid  30909  blocnilem  31193  htthlem  31306  nmcexi  32415  dmdbr3  32694  dmdbr4  32695  atom1d  32742  dvelimalcased  35495  dvelimexcased  35497  mclsax  36082  dfon2lem8  36301  nn0prpwlem  36874  bj-ceqsalt0  37560  bj-ceqsalt1  37561  filbcmb  38432  divrngidl  38720  lshpcmp  39803  lsat0cv  39848  atnle  40132  lpolconN  42302  ss2iundf  44426  iccpartdisj  48227  lighneallem2  48399  lighneallem3  48400  lighneallem4  48403  proththd  48407  sgoldbeven3prm  48589  bgoldbtbndlem2  48612  upgrimwlklem5  48707  upgrwlkupwlk  48946  lindslinindsimp1  49278  nn0sumshdiglemA  49440  eenglngeehlnmlem2  49559  setrec1lem4  50509