Theorem mpid 43

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 42	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  47  pm2.43a  52  embantd  57  mtord  690  mpan2d  706  ceqsalt  3201  rspcimdv  3283  riotass2  6537  peano5  6981  oeordi  7554  isf34lem4  9082  domtriomlem  9147  axcclem  9162  ssnn0fi  12646  repswrevw  13384  rlimcn1  14167  climcn1  14170  climcn2  14171  dvdsgcd  15099  lcmfunsnlem2lem1  15189  coprmgcdb  15200  nprm  15239  pcqmul  15396  prmgaplem7  15599  lubun  16946  grpid  17280  psgnunilem4  17740  gexdvds  17822  scmate  20135  cayleyhamilton1  20516  uniopn  20527  tgcmp  21014  uncmp  21016  nconsubb  21036  comppfsc  21145  kgencn2  21170  isufil2  21522  cfinufil  21542  fin1aufil  21546  flimopn  21589  cnpflf  21615  flimfnfcls  21642  fcfnei  21649  metcnp3  22155  cncfco  22518  ellimc3  23449  dvfsumrlim  23598  cxploglim  24504  constr3trllem2  26179  frgrancvvdeqlemB  26565  grpoid  26758  blocnilem  27043  htthlem  27158  nmcexi  28269  dmdbr3  28548  dmdbr4  28549  atom1d  28596  mclsax  30720  dfon2lem8  30939  nn0prpwlem  31487  nn0prpw  31488  bj-ceqsalt0  32067  bj-ceqsalt1  32068  filbcmb  32705  divrngidl  32997  lshpcmp  33293  lsat0cv  33338  atnle  33622  lpolconN  35794  ss2iundf  36970  iccpartdisj  39975  lighneallem2  40061  lighneallem3  40062  lighneallem4  40065  proththd  40069  bgoldbtbndlem2  40222  nbuhgr2vtx1edgblem  40573  nbusgrvtxm1  40607  upgr1wlkwlk  40847  1wlkp1lem6  40887  pthdlem2lem  40973  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  wwlks2onv  41158  eupth2  41407  frgrncvvdeqlemB  41477  lindslinindsimp1  42040  nn0sumshdiglemA  42211  setrec1lem4  42236