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  3568  riotass2  7355  peano5  7845  oeordi  8525  isf34lem4  10299  domtriomlem  10364  axcclem  10379  ssnn0fi  13920  repswrevw  14722  rlimcn1  15523  climcn1  15527  climcn2  15528  dvdsgcd  16483  lcmfunsnlem2lem1  16577  coprmgcdb  16588  nprm  16627  pcqmul  16793  prmgaplem7  16997  lubun  18450  grpid  18917  psgnunilem4  19438  gexdvds  19525  rngqiprngfulem2  21279  rngqipring1  21283  scmate  22466  cayleyhamilton1  22848  uniopn  22853  tgcmp  23357  uncmp  23359  nconnsubb  23379  comppfsc  23488  kgencn2  23513  isufil2  23864  cfinufil  23884  fin1aufil  23888  flimopn  23931  cnpflf  23957  flimfnfcls  23984  fcfnei  23991  metcnp3  24496  cncfco  24868  ellimc3  25848  dvfsumrlim  26006  cxploglim  26956  2sqreultblem  27427  nbuhgr2vtx1edgblem  29436  nbusgrvtxm1  29464  wlkp1lem6  29762  pthdlem2lem  29852  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  wlknwwlksnbij  29973  eupth2  30326  frgrncvvdeqlem8  30393  grpoid  30607  blocnilem  30891  htthlem  31004  nmcexi  32113  dmdbr3  32392  dmdbr4  32393  atom1d  32440  dvelimalcased  35250  dvelimexcased  35252  mclsax  35782  dfon2lem8  36001  nn0prpwlem  36535  bj-ceqsalt0  37126  bj-ceqsalt1  37127  filbcmb  37985  divrngidl  38273  lshpcmp  39358  lsat0cv  39403  atnle  39687  lpolconN  41857  ss2iundf  44009  iccpartdisj  47791  lighneallem2  47960  lighneallem3  47961  lighneallem4  47964  proththd  47968  sgoldbeven3prm  48137  bgoldbtbndlem2  48160  upgrimwlklem5  48255  upgrwlkupwlk  48494  lindslinindsimp1  48811  nn0sumshdiglemA  48973  eenglngeehlnmlem2  49092  setrec1lem4  50043