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  681  mtord  863  ceqsalt  3448  rspcimdv  3536  riotass2  6966  peano5  7422  oeordi  8016  isf34lem4  9599  domtriomlem  9664  axcclem  9679  ssnn0fi  13171  repswrevw  14009  rlimcn1  14809  climcn1  14812  climcn2  14813  dvdsgcd  15751  lcmfunsnlem2lem1  15841  coprmgcdb  15852  nprm  15891  pcqmul  16049  prmgaplem7  16252  lubun  17594  grpid  17929  psgnunilem4  18390  gexdvds  18473  scmate  20826  cayleyhamilton1  21207  uniopn  21212  tgcmp  21716  uncmp  21718  nconnsubb  21738  comppfsc  21847  kgencn2  21872  isufil2  22223  cfinufil  22243  fin1aufil  22247  flimopn  22290  cnpflf  22316  flimfnfcls  22343  fcfnei  22350  metcnp3  22856  cncfco  23221  ellimc3  24183  dvfsumrlim  24334  cxploglim  25260  2sqreultblem  25729  nbuhgr2vtx1edgblem  26839  nbusgrvtxm1  26867  wlkp1lem6  27169  pthdlem2lem  27259  crctcshwlkn0lem4  27302  crctcshwlkn0lem5  27303  wlknwwlksnbij  27378  eupth2  27772  frgrncvvdeqlem8  27843  grpoid  28077  blocnilem  28361  htthlem  28476  nmcexi  29587  dmdbr3  29866  dmdbr4  29867  atom1d  29914  mclsax  32336  dfon2lem8  32555  nn0prpwlem  33191  bj-ceqsalt0  33693  bj-ceqsalt1  33694  filbcmb  34457  divrngidl  34748  lshpcmp  35569  lsat0cv  35614  atnle  35898  lpolconN  38068  ss2iundf  39367  iccpartdisj  42970  lighneallem2  43140  lighneallem3  43141  lighneallem4  43144  proththd  43148  sgoldbeven3prm  43317  bgoldbtbndlem2  43340  upgrwlkupwlk  43384  lindslinindsimp1  43880  nn0sumshdiglemA  44048  eenglngeehlnmlem2  44094  setrec1lem4  44161