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  3612  riotass2  7418  peano5  7915  oeordi  8625  isf34lem4  10417  domtriomlem  10482  axcclem  10497  ssnn0fi  14026  repswrevw  14825  rlimcn1  15624  climcn1  15628  climcn2  15629  dvdsgcd  16581  lcmfunsnlem2lem1  16675  coprmgcdb  16686  nprm  16725  pcqmul  16891  prmgaplem7  17095  lubun  18560  grpid  18993  psgnunilem4  19515  gexdvds  19602  rngqiprngfulem2  21322  rngqipring1  21326  scmate  22516  cayleyhamilton1  22898  uniopn  22903  tgcmp  23409  uncmp  23411  nconnsubb  23431  comppfsc  23540  kgencn2  23565  isufil2  23916  cfinufil  23936  fin1aufil  23940  flimopn  23983  cnpflf  24009  flimfnfcls  24036  fcfnei  24043  metcnp3  24553  cncfco  24933  ellimc3  25914  dvfsumrlim  26072  cxploglim  27021  2sqreultblem  27492  nbuhgr2vtx1edgblem  29368  nbusgrvtxm1  29396  wlkp1lem6  29696  pthdlem2lem  29787  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  wlknwwlksnbij  29908  eupth2  30258  frgrncvvdeqlem8  30325  grpoid  30539  blocnilem  30823  htthlem  30936  nmcexi  32045  dmdbr3  32324  dmdbr4  32325  atom1d  32372  dvelimalcased  35089  dvelimexcased  35091  mclsax  35574  dfon2lem8  35791  nn0prpwlem  36323  bj-ceqsalt0  36885  bj-ceqsalt1  36886  filbcmb  37747  divrngidl  38035  lshpcmp  38989  lsat0cv  39034  atnle  39318  lpolconN  41489  ss2iundf  43672  iccpartdisj  47424  lighneallem2  47593  lighneallem3  47594  lighneallem4  47597  proththd  47601  sgoldbeven3prm  47770  bgoldbtbndlem2  47793  upgrwlkupwlk  48056  lindslinindsimp1  48374  nn0sumshdiglemA  48540  eenglngeehlnmlem2  48659  setrec1lem4  49209