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  693  rspcimdv  3603  riotass2  7396  peano5  7884  peano5OLD  7885  oeordi  8587  isf34lem4  10372  domtriomlem  10437  axcclem  10452  ssnn0fi  13950  repswrevw  14737  rlimcn1  15532  climcn1  15536  climcn2  15537  dvdsgcd  16486  lcmfunsnlem2lem1  16575  coprmgcdb  16586  nprm  16625  pcqmul  16786  prmgaplem7  16990  lubun  18468  grpid  18860  psgnunilem4  19365  gexdvds  19452  scmate  22012  cayleyhamilton1  22394  uniopn  22399  tgcmp  22905  uncmp  22907  nconnsubb  22927  comppfsc  23036  kgencn2  23061  isufil2  23412  cfinufil  23432  fin1aufil  23436  flimopn  23479  cnpflf  23505  flimfnfcls  23532  fcfnei  23539  metcnp3  24049  cncfco  24423  ellimc3  25396  dvfsumrlim  25548  cxploglim  26482  2sqreultblem  26951  nbuhgr2vtx1edgblem  28608  nbusgrvtxm1  28636  wlkp1lem6  28935  pthdlem2lem  29024  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  wlknwwlksnbij  29142  eupth2  29492  frgrncvvdeqlem8  29559  grpoid  29773  blocnilem  30057  htthlem  30170  nmcexi  31279  dmdbr3  31558  dmdbr4  31559  atom1d  31606  mclsax  34560  dfon2lem8  34762  nn0prpwlem  35207  bj-ceqsalt0  35764  bj-ceqsalt1  35765  filbcmb  36608  divrngidl  36896  lshpcmp  37858  lsat0cv  37903  atnle  38187  lpolconN  40358  ss2iundf  42410  iccpartdisj  46105  lighneallem2  46274  lighneallem3  46275  lighneallem4  46278  proththd  46282  sgoldbeven3prm  46451  bgoldbtbndlem2  46474  upgrwlkupwlk  46518  rngqiprngfulem2  46797  rngqipring1  46801  lindslinindsimp1  47138  nn0sumshdiglemA  47305  eenglngeehlnmlem2  47424  setrec1lem4  47735