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  700  rspcimdv  3557  riotass2  7350  peano5  7840  oeordi  8520  isf34lem4  10297  domtriomlem  10362  axcclem  10377  ssnn0fi  13945  repswrevw  14747  rlimcn1  15548  climcn1  15552  climcn2  15553  dvdsgcd  16511  lcmfunsnlem2lem1  16605  coprmgcdb  16616  nprm  16655  pcqmul  16822  prmgaplem7  17026  lubun  18479  grpid  18949  psgnunilem4  19470  gexdvds  19557  rngqiprngfulem2  21312  rngqipring1  21316  scmate  22500  cayleyhamilton1  22882  uniopn  22887  tgcmp  23391  uncmp  23393  nconnsubb  23413  comppfsc  23522  kgencn2  23547  isufil2  23898  cfinufil  23918  fin1aufil  23922  flimopn  23965  cnpflf  23991  flimfnfcls  24018  fcfnei  24025  metcnp3  24530  cncfco  24899  ellimc3  25871  dvfsumrlim  26023  cxploglim  26966  2sqreultblem  27436  nbuhgr2vtx1edgblem  29445  nbusgrvtxm1  29473  wlkp1lem6  29770  pthdlem2lem  29860  crctcshwlkn0lem4  29906  crctcshwlkn0lem5  29907  wlknwwlksnbij  29981  eupth2  30334  frgrncvvdeqlem8  30401  grpoid  30616  blocnilem  30900  htthlem  31013  nmcexi  32122  dmdbr3  32401  dmdbr4  32402  atom1d  32449  dvelimalcased  35264  dvelimexcased  35266  mclsax  35804  dfon2lem8  36023  nn0prpwlem  36557  bj-ceqsalt0  37244  bj-ceqsalt1  37245  filbcmb  38114  divrngidl  38402  lshpcmp  39487  lsat0cv  39532  atnle  39816  lpolconN  41986  ss2iundf  44110  iccpartdisj  47919  lighneallem2  48091  lighneallem3  48092  lighneallem4  48095  proththd  48099  sgoldbeven3prm  48281  bgoldbtbndlem2  48304  upgrimwlklem5  48399  upgrwlkupwlk  48638  lindslinindsimp1  48955  nn0sumshdiglemA  49117  eenglngeehlnmlem2  49236  setrec1lem4  50187