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  3527  rspcimdv  3613  riotass2  7144  peano5  7605  oeordi  8213  isf34lem4  9799  domtriomlem  9864  axcclem  9879  ssnn0fi  13354  repswrevw  14149  rlimcn1  14945  climcn1  14948  climcn2  14949  dvdsgcd  15892  lcmfunsnlem2lem1  15982  coprmgcdb  15993  nprm  16032  pcqmul  16190  prmgaplem7  16393  lubun  17733  grpid  18139  psgnunilem4  18625  gexdvds  18709  scmate  21119  cayleyhamilton1  21500  uniopn  21505  tgcmp  22009  uncmp  22011  nconnsubb  22031  comppfsc  22140  kgencn2  22165  isufil2  22516  cfinufil  22536  fin1aufil  22540  flimopn  22583  cnpflf  22609  flimfnfcls  22636  fcfnei  22643  metcnp3  23150  cncfco  23515  ellimc3  24477  dvfsumrlim  24628  cxploglim  25555  2sqreultblem  26024  nbuhgr2vtx1edgblem  27133  nbusgrvtxm1  27161  wlkp1lem6  27460  pthdlem2lem  27548  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  wlknwwlksnbij  27666  eupth2  28018  frgrncvvdeqlem8  28085  grpoid  28297  blocnilem  28581  htthlem  28694  nmcexi  29803  dmdbr3  30082  dmdbr4  30083  atom1d  30130  mclsax  32816  dfon2lem8  33035  nn0prpwlem  33670  bj-ceqsalt0  34203  bj-ceqsalt1  34204  filbcmb  35030  divrngidl  35321  lshpcmp  36139  lsat0cv  36184  atnle  36468  lpolconN  38638  ss2iundf  40053  iccpartdisj  43646  lighneallem2  43820  lighneallem3  43821  lighneallem4  43824  proththd  43828  sgoldbeven3prm  43997  bgoldbtbndlem2  44020  upgrwlkupwlk  44064  lindslinindsimp1  44561  nn0sumshdiglemA  44728  eenglngeehlnmlem2  44774  setrec1lem4  44842