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  695  rspcimdv  3554  riotass2  7354  peano5  7844  oeordi  8523  isf34lem4  10299  domtriomlem  10364  axcclem  10379  ssnn0fi  13947  repswrevw  14749  rlimcn1  15550  climcn1  15554  climcn2  15555  dvdsgcd  16513  lcmfunsnlem2lem1  16607  coprmgcdb  16618  nprm  16657  pcqmul  16824  prmgaplem7  17028  lubun  18481  grpid  18951  psgnunilem4  19472  gexdvds  19559  rngqiprngfulem2  21310  rngqipring1  21314  scmate  22475  cayleyhamilton1  22857  uniopn  22862  tgcmp  23366  uncmp  23368  nconnsubb  23388  comppfsc  23497  kgencn2  23522  isufil2  23873  cfinufil  23893  fin1aufil  23897  flimopn  23940  cnpflf  23966  flimfnfcls  23993  fcfnei  24000  metcnp3  24505  cncfco  24874  ellimc3  25846  dvfsumrlim  25998  cxploglim  26941  2sqreultblem  27411  nbuhgr2vtx1edgblem  29420  nbusgrvtxm1  29448  wlkp1lem6  29745  pthdlem2lem  29835  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  wlknwwlksnbij  29956  eupth2  30309  frgrncvvdeqlem8  30376  grpoid  30591  blocnilem  30875  htthlem  30988  nmcexi  32097  dmdbr3  32376  dmdbr4  32377  atom1d  32424  dvelimalcased  35217  dvelimexcased  35219  mclsax  35751  dfon2lem8  35970  nn0prpwlem  36504  bj-ceqsalt0  37191  bj-ceqsalt1  37192  filbcmb  38061  divrngidl  38349  lshpcmp  39434  lsat0cv  39479  atnle  39763  lpolconN  41933  ss2iundf  44086  iccpartdisj  47897  lighneallem2  48069  lighneallem3  48070  lighneallem4  48073  proththd  48077  sgoldbeven3prm  48259  bgoldbtbndlem2  48282  upgrimwlklem5  48377  upgrwlkupwlk  48616  lindslinindsimp1  48933  nn0sumshdiglemA  49095  eenglngeehlnmlem2  49214  setrec1lem4  50165