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  3591  riotass2  7390  peano5  7887  oeordi  8597  isf34lem4  10389  domtriomlem  10454  axcclem  10469  ssnn0fi  14001  repswrevw  14803  rlimcn1  15602  climcn1  15606  climcn2  15607  dvdsgcd  16561  lcmfunsnlem2lem1  16655  coprmgcdb  16666  nprm  16705  pcqmul  16871  prmgaplem7  17075  lubun  18523  grpid  18956  psgnunilem4  19476  gexdvds  19563  rngqiprngfulem2  21271  rngqipring1  21275  scmate  22446  cayleyhamilton1  22828  uniopn  22833  tgcmp  23337  uncmp  23339  nconnsubb  23359  comppfsc  23468  kgencn2  23493  isufil2  23844  cfinufil  23864  fin1aufil  23868  flimopn  23911  cnpflf  23937  flimfnfcls  23964  fcfnei  23971  metcnp3  24477  cncfco  24849  ellimc3  25830  dvfsumrlim  25988  cxploglim  26938  2sqreultblem  27409  nbuhgr2vtx1edgblem  29276  nbusgrvtxm1  29304  wlkp1lem6  29604  pthdlem2lem  29695  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  wlknwwlksnbij  29816  eupth2  30166  frgrncvvdeqlem8  30233  grpoid  30447  blocnilem  30731  htthlem  30844  nmcexi  31953  dmdbr3  32232  dmdbr4  32233  atom1d  32280  dvelimalcased  35052  dvelimexcased  35054  mclsax  35537  dfon2lem8  35754  nn0prpwlem  36286  bj-ceqsalt0  36848  bj-ceqsalt1  36849  filbcmb  37710  divrngidl  37998  lshpcmp  38952  lsat0cv  38997  atnle  39281  lpolconN  41452  ss2iundf  43630  iccpartdisj  47399  lighneallem2  47568  lighneallem3  47569  lighneallem4  47572  proththd  47576  sgoldbeven3prm  47745  bgoldbtbndlem2  47768  upgrimwlklem5  47862  upgrwlkupwlk  48063  lindslinindsimp1  48381  nn0sumshdiglemA  48547  eenglngeehlnmlem2  48666  setrec1lem4  49502