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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mp2d  50  pm2.43a  55  embantd  60  mpan2d  707  rspcimdv  3566  riotass2  7407  peano5  7905  oeordi  8599  setrec1lem4  9974  isf34lem4  10458  domtriomlem  10523  axcclem  10538  ssnn0fi  14131  repswrevw  14942  rlimcn1  15760  climcn1  15764  climcn2  15765  dvdsgcd  16722  lcmfunsnlem2lem1  16818  coprmgcdb  16829  nprm  16868  pcqmul  17036  prmgaplem7  17240  lubun  18694  grpid  19191  psgnunilem4  19716  gexdvds  19803  rngqiprngfulem2  21613  rngqipring1  21617  scmate  22830  cayleyhamilton1  23215  uniopn  23220  tgcmp  23724  uncmp  23726  nconnsubb  23746  comppfsc  23856  kgencn2  23881  isufil2  24232  cfinufil  24252  fin1aufil  24256  flimopn  24299  cnpflf  24325  flimfnfcls  24352  fcfnei  24359  metcnp3  24864  cncfco  25233  ellimc3  26204  dvfsumrlim  26356  cxploglim  27310  2sqreultblem  27780  nbuhgr2vtx1edgblem  29937  nbusgrvtxm1  29965  wlkp1lem6  30262  pthdlem2lem  30358  crctcshwlkn0lem4  30407  crctcshwlkn0lem5  30408  wlknwwlksnbij  30482  eupth2  30845  frgrncvvdeqlem8  30912  grpoid  31127  blocnilem  31411  htthlem  31524  nmcexi  32633  dmdbr3  32912  dmdbr4  32913  atom1d  32960  dvelimalcased  35751  dvelimexcased  35753  mclsax  36420  dfon2lem8  36644  nn0prpwlem  37202  bj-ceqsalt0  37888  bj-ceqsalt1  37889  filbcmb  38767  divrngidl  39055  lshpcmp  40138  lsat0cv  40183  atnle  40467  lpolconN  42637  ss2iundf  44752  iccpartdisj  48612  lighneallem2  48784  lighneallem3  48785  lighneallem4  48788  proththd  48792  sgoldbeven3prm  48974  bgoldbtbndlem2  48997  upgrimwlklem5  49092  upgrwlkupwlk  49331  lindslinindsimp1  49662  nn0sumshdiglemA  49824  eenglngeehlnmlem2  49944  nellindf  51138