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  694  rspcimdv  3567  riotass2  7333  peano5  7823  oeordi  8502  isf34lem4  10265  domtriomlem  10330  axcclem  10345  ssnn0fi  13889  repswrevw  14691  rlimcn1  15492  climcn1  15496  climcn2  15497  dvdsgcd  16452  lcmfunsnlem2lem1  16546  coprmgcdb  16557  nprm  16596  pcqmul  16762  prmgaplem7  16966  lubun  18418  grpid  18885  psgnunilem4  19407  gexdvds  19494  rngqiprngfulem2  21247  rngqipring1  21251  scmate  22423  cayleyhamilton1  22805  uniopn  22810  tgcmp  23314  uncmp  23316  nconnsubb  23336  comppfsc  23445  kgencn2  23470  isufil2  23821  cfinufil  23841  fin1aufil  23845  flimopn  23888  cnpflf  23914  flimfnfcls  23941  fcfnei  23948  metcnp3  24453  cncfco  24825  ellimc3  25805  dvfsumrlim  25963  cxploglim  26913  2sqreultblem  27384  nbuhgr2vtx1edgblem  29327  nbusgrvtxm1  29355  wlkp1lem6  29653  pthdlem2lem  29743  crctcshwlkn0lem4  29789  crctcshwlkn0lem5  29790  wlknwwlksnbij  29864  eupth2  30214  frgrncvvdeqlem8  30281  grpoid  30495  blocnilem  30779  htthlem  30892  nmcexi  32001  dmdbr3  32280  dmdbr4  32281  atom1d  32328  dvelimalcased  35082  dvelimexcased  35084  mclsax  35601  dfon2lem8  35823  nn0prpwlem  36355  bj-ceqsalt0  36917  bj-ceqsalt1  36918  filbcmb  37779  divrngidl  38067  lshpcmp  39026  lsat0cv  39071  atnle  39355  lpolconN  41525  ss2iundf  43691  iccpartdisj  47467  lighneallem2  47636  lighneallem3  47637  lighneallem4  47640  proththd  47644  sgoldbeven3prm  47813  bgoldbtbndlem2  47836  upgrimwlklem5  47931  upgrwlkupwlk  48170  lindslinindsimp1  48488  nn0sumshdiglemA  48650  eenglngeehlnmlem2  48769  setrec1lem4  49721