Theorem mpid 44

Description: A nested modus ponens deduction. Deduction associated with mpi 20. (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 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		mpid.2	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	2, 3	mpdd 43	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  49  pm2.43a  54  embantd  59  mpan2d  694  rspcimdv  3578  riotass2  7374  peano5  7869  oeordi  8551  isf34lem4  10330  domtriomlem  10395  axcclem  10410  ssnn0fi  13950  repswrevw  14752  rlimcn1  15554  climcn1  15558  climcn2  15559  dvdsgcd  16514  lcmfunsnlem2lem1  16608  coprmgcdb  16619  nprm  16658  pcqmul  16824  prmgaplem7  17028  lubun  18474  grpid  18907  psgnunilem4  19427  gexdvds  19514  rngqiprngfulem2  21222  rngqipring1  21226  scmate  22397  cayleyhamilton1  22779  uniopn  22784  tgcmp  23288  uncmp  23290  nconnsubb  23310  comppfsc  23419  kgencn2  23444  isufil2  23795  cfinufil  23815  fin1aufil  23819  flimopn  23862  cnpflf  23888  flimfnfcls  23915  fcfnei  23922  metcnp3  24428  cncfco  24800  ellimc3  25780  dvfsumrlim  25938  cxploglim  26888  2sqreultblem  27359  nbuhgr2vtx1edgblem  29278  nbusgrvtxm1  29306  wlkp1lem6  29606  pthdlem2lem  29697  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  wlknwwlksnbij  29818  eupth2  30168  frgrncvvdeqlem8  30235  grpoid  30449  blocnilem  30733  htthlem  30846  nmcexi  31955  dmdbr3  32234  dmdbr4  32235  atom1d  32282  dvelimalcased  35065  dvelimexcased  35067  mclsax  35556  dfon2lem8  35778  nn0prpwlem  36310  bj-ceqsalt0  36872  bj-ceqsalt1  36873  filbcmb  37734  divrngidl  38022  lshpcmp  38981  lsat0cv  39026  atnle  39310  lpolconN  41481  ss2iundf  43648  iccpartdisj  47438  lighneallem2  47607  lighneallem3  47608  lighneallem4  47611  proththd  47615  sgoldbeven3prm  47784  bgoldbtbndlem2  47807  upgrimwlklem5  47901  upgrwlkupwlk  48128  lindslinindsimp1  48446  nn0sumshdiglemA  48608  eenglngeehlnmlem2  48727  setrec1lem4  49679