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  3569  riotass2  7340  peano5  7833  oeordi  8512  isf34lem4  10290  domtriomlem  10355  axcclem  10370  ssnn0fi  13910  repswrevw  14711  rlimcn1  15513  climcn1  15517  climcn2  15518  dvdsgcd  16473  lcmfunsnlem2lem1  16567  coprmgcdb  16578  nprm  16617  pcqmul  16783  prmgaplem7  16987  lubun  18439  grpid  18872  psgnunilem4  19394  gexdvds  19481  rngqiprngfulem2  21237  rngqipring1  21241  scmate  22413  cayleyhamilton1  22795  uniopn  22800  tgcmp  23304  uncmp  23306  nconnsubb  23326  comppfsc  23435  kgencn2  23460  isufil2  23811  cfinufil  23831  fin1aufil  23835  flimopn  23878  cnpflf  23904  flimfnfcls  23931  fcfnei  23938  metcnp3  24444  cncfco  24816  ellimc3  25796  dvfsumrlim  25954  cxploglim  26904  2sqreultblem  27375  nbuhgr2vtx1edgblem  29314  nbusgrvtxm1  29342  wlkp1lem6  29640  pthdlem2lem  29730  crctcshwlkn0lem4  29776  crctcshwlkn0lem5  29777  wlknwwlksnbij  29851  eupth2  30201  frgrncvvdeqlem8  30268  grpoid  30482  blocnilem  30766  htthlem  30879  nmcexi  31988  dmdbr3  32267  dmdbr4  32268  atom1d  32315  dvelimalcased  35041  dvelimexcased  35043  mclsax  35541  dfon2lem8  35763  nn0prpwlem  36295  bj-ceqsalt0  36857  bj-ceqsalt1  36858  filbcmb  37719  divrngidl  38007  lshpcmp  38966  lsat0cv  39011  atnle  39295  lpolconN  41466  ss2iundf  43632  iccpartdisj  47422  lighneallem2  47591  lighneallem3  47592  lighneallem4  47595  proththd  47599  sgoldbeven3prm  47768  bgoldbtbndlem2  47791  upgrimwlklem5  47886  upgrwlkupwlk  48125  lindslinindsimp1  48443  nn0sumshdiglemA  48605  eenglngeehlnmlem2  48724  setrec1lem4  49676