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  691  rspcimdv  3602  riotass2  7399  peano5  7888  peano5OLD  7889  oeordi  8593  isf34lem4  10378  domtriomlem  10443  axcclem  10458  ssnn0fi  13957  repswrevw  14744  rlimcn1  15539  climcn1  15543  climcn2  15544  dvdsgcd  16493  lcmfunsnlem2lem1  16582  coprmgcdb  16593  nprm  16632  pcqmul  16793  prmgaplem7  16997  lubun  18478  grpid  18903  psgnunilem4  19413  gexdvds  19500  rngqiprngfulem2  21160  rngqipring1  21164  scmate  22332  cayleyhamilton1  22714  uniopn  22719  tgcmp  23225  uncmp  23227  nconnsubb  23247  comppfsc  23356  kgencn2  23381  isufil2  23732  cfinufil  23752  fin1aufil  23756  flimopn  23799  cnpflf  23825  flimfnfcls  23852  fcfnei  23859  metcnp3  24369  cncfco  24747  ellimc3  25728  dvfsumrlim  25886  cxploglim  26823  2sqreultblem  27294  nbuhgr2vtx1edgblem  29041  nbusgrvtxm1  29069  wlkp1lem6  29368  pthdlem2lem  29457  crctcshwlkn0lem4  29500  crctcshwlkn0lem5  29501  wlknwwlksnbij  29575  eupth2  29925  frgrncvvdeqlem8  29992  grpoid  30206  blocnilem  30490  htthlem  30603  nmcexi  31712  dmdbr3  31991  dmdbr4  31992  atom1d  32039  mclsax  35024  dfon2lem8  35232  nn0prpwlem  35671  bj-ceqsalt0  36228  bj-ceqsalt1  36229  filbcmb  37072  divrngidl  37360  lshpcmp  38322  lsat0cv  38367  atnle  38651  lpolconN  40822  ss2iundf  42873  iccpartdisj  46564  lighneallem2  46733  lighneallem3  46734  lighneallem4  46737  proththd  46741  sgoldbeven3prm  46910  bgoldbtbndlem2  46933  upgrwlkupwlk  46977  lindslinindsimp1  47300  nn0sumshdiglemA  47467  eenglngeehlnmlem2  47586  setrec1lem4  47897