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  690  ceqsalt  3452  rspcimdv  3541  riotass2  7243  peano5  7714  peano5OLD  7715  oeordi  8380  isf34lem4  10064  domtriomlem  10129  axcclem  10144  ssnn0fi  13633  repswrevw  14428  rlimcn1  15225  climcn1  15229  climcn2  15230  dvdsgcd  16180  lcmfunsnlem2lem1  16271  coprmgcdb  16282  nprm  16321  pcqmul  16482  prmgaplem7  16686  lubun  18148  grpid  18530  psgnunilem4  19020  gexdvds  19104  scmate  21567  cayleyhamilton1  21949  uniopn  21954  tgcmp  22460  uncmp  22462  nconnsubb  22482  comppfsc  22591  kgencn2  22616  isufil2  22967  cfinufil  22987  fin1aufil  22991  flimopn  23034  cnpflf  23060  flimfnfcls  23087  fcfnei  23094  metcnp3  23602  cncfco  23976  ellimc3  24948  dvfsumrlim  25100  cxploglim  26032  2sqreultblem  26501  nbuhgr2vtx1edgblem  27621  nbusgrvtxm1  27649  wlkp1lem6  27948  pthdlem2lem  28036  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  wlknwwlksnbij  28154  eupth2  28504  frgrncvvdeqlem8  28571  grpoid  28783  blocnilem  29067  htthlem  29180  nmcexi  30289  dmdbr3  30568  dmdbr4  30569  atom1d  30616  mclsax  33431  dfon2lem8  33672  nn0prpwlem  34438  bj-ceqsalt0  34996  bj-ceqsalt1  34997  filbcmb  35825  divrngidl  36113  lshpcmp  36929  lsat0cv  36974  atnle  37258  lpolconN  39428  ss2iundf  41156  iccpartdisj  44777  lighneallem2  44946  lighneallem3  44947  lighneallem4  44950  proththd  44954  sgoldbeven3prm  45123  bgoldbtbndlem2  45146  upgrwlkupwlk  45190  lindslinindsimp1  45686  nn0sumshdiglemA  45853  eenglngeehlnmlem2  45972  setrec1lem4  46282