Theorem mpid 45

Description: A nested modus ponens deduction. Deduction associated with mpi 21. (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 26	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		mpid.2	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	2, 3	mpdd 44	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  50  pm2.43a  55  embantd  60  mpan2d  706  rspcimdv  3574  riotass2  7387  peano5  7878  oeordi  8561  isf34lem4  10349  domtriomlem  10414  axcclem  10429  ssnn0fi  14012  repswrevw  14814  rlimcn1  15629  climcn1  15633  climcn2  15634  dvdsgcd  16592  lcmfunsnlem2lem1  16686  coprmgcdb  16697  nprm  16736  pcqmul  16903  prmgaplem7  17107  lubun  18561  grpid  19032  psgnunilem4  19558  gexdvds  19645  rngqiprngfulem2  21414  rngqipring1  21418  scmate  22628  cayleyhamilton1  23010  uniopn  23015  tgcmp  23519  uncmp  23521  nconnsubb  23541  comppfsc  23650  kgencn2  23675  isufil2  24026  cfinufil  24046  fin1aufil  24050  flimopn  24093  cnpflf  24119  flimfnfcls  24146  fcfnei  24153  metcnp3  24658  cncfco  25027  ellimc3  25999  dvfsumrlim  26151  cxploglim  27100  2sqreultblem  27570  nbuhgr2vtx1edgblem  29610  nbusgrvtxm1  29638  wlkp1lem6  29935  pthdlem2lem  30025  crctcshwlkn0lem4  30071  crctcshwlkn0lem5  30072  wlknwwlksnbij  30146  eupth2  30499  frgrncvvdeqlem8  30566  grpoid  30781  blocnilem  31065  htthlem  31178  nmcexi  32287  dmdbr3  32566  dmdbr4  32567  atom1d  32614  dvelimalcased  35380  dvelimexcased  35382  mclsax  35932  dfon2lem8  36151  nn0prpwlem  36695  bj-ceqsalt0  37381  bj-ceqsalt1  37382  filbcmb  38251  divrngidl  38539  lshpcmp  39624  lsat0cv  39669  atnle  39953  lpolconN  42123  ss2iundf  44247  iccpartdisj  48041  lighneallem2  48213  lighneallem3  48214  lighneallem4  48217  proththd  48221  sgoldbeven3prm  48403  bgoldbtbndlem2  48426  upgrimwlklem5  48521  upgrwlkupwlk  48760  lindslinindsimp1  49088  nn0sumshdiglemA  49250  eenglngeehlnmlem2  49369  setrec1lem4  50319