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  692  ceqsalt  3529  rspcimdv  3615  riotass2  7146  peano5  7607  oeordi  8215  isf34lem4  9801  domtriomlem  9866  axcclem  9881  ssnn0fi  13356  repswrevw  14151  rlimcn1  14947  climcn1  14950  climcn2  14951  dvdsgcd  15894  lcmfunsnlem2lem1  15984  coprmgcdb  15995  nprm  16034  pcqmul  16192  prmgaplem7  16395  lubun  17735  grpid  18141  psgnunilem4  18627  gexdvds  18711  scmate  21121  cayleyhamilton1  21502  uniopn  21507  tgcmp  22011  uncmp  22013  nconnsubb  22033  comppfsc  22142  kgencn2  22167  isufil2  22518  cfinufil  22538  fin1aufil  22542  flimopn  22585  cnpflf  22611  flimfnfcls  22638  fcfnei  22645  metcnp3  23152  cncfco  23517  ellimc3  24479  dvfsumrlim  24630  cxploglim  25557  2sqreultblem  26026  nbuhgr2vtx1edgblem  27135  nbusgrvtxm1  27163  wlkp1lem6  27462  pthdlem2lem  27550  crctcshwlkn0lem4  27593  crctcshwlkn0lem5  27594  wlknwwlksnbij  27668  eupth2  28020  frgrncvvdeqlem8  28087  grpoid  28299  blocnilem  28583  htthlem  28696  nmcexi  29805  dmdbr3  30084  dmdbr4  30085  atom1d  30132  mclsax  32818  dfon2lem8  33037  nn0prpwlem  33672  bj-ceqsalt0  34202  bj-ceqsalt1  34203  filbcmb  35017  divrngidl  35308  lshpcmp  36126  lsat0cv  36171  atnle  36455  lpolconN  38625  ss2iundf  40011  iccpartdisj  43604  lighneallem2  43778  lighneallem3  43779  lighneallem4  43782  proththd  43786  sgoldbeven3prm  43955  bgoldbtbndlem2  43978  upgrwlkupwlk  44022  lindslinindsimp1  44519  nn0sumshdiglemA  44686  eenglngeehlnmlem2  44732  setrec1lem4  44800