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  691  ceqsalt  3463  rspcimdv  3552  riotass2  7272  peano5  7749  peano5OLD  7750  oeordi  8427  isf34lem4  10142  domtriomlem  10207  axcclem  10222  ssnn0fi  13714  repswrevw  14509  rlimcn1  15306  climcn1  15310  climcn2  15311  dvdsgcd  16261  lcmfunsnlem2lem1  16352  coprmgcdb  16363  nprm  16402  pcqmul  16563  prmgaplem7  16767  lubun  18242  grpid  18624  psgnunilem4  19114  gexdvds  19198  scmate  21668  cayleyhamilton1  22050  uniopn  22055  tgcmp  22561  uncmp  22563  nconnsubb  22583  comppfsc  22692  kgencn2  22717  isufil2  23068  cfinufil  23088  fin1aufil  23092  flimopn  23135  cnpflf  23161  flimfnfcls  23188  fcfnei  23195  metcnp3  23705  cncfco  24079  ellimc3  25052  dvfsumrlim  25204  cxploglim  26136  2sqreultblem  26605  nbuhgr2vtx1edgblem  27727  nbusgrvtxm1  27755  wlkp1lem6  28055  pthdlem2lem  28144  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  wlknwwlksnbij  28262  eupth2  28612  frgrncvvdeqlem8  28679  grpoid  28891  blocnilem  29175  htthlem  29288  nmcexi  30397  dmdbr3  30676  dmdbr4  30677  atom1d  30724  mclsax  33540  dfon2lem8  33775  nn0prpwlem  34520  bj-ceqsalt0  35078  bj-ceqsalt1  35079  filbcmb  35907  divrngidl  36195  lshpcmp  37009  lsat0cv  37054  atnle  37338  lpolconN  39508  ss2iundf  41274  iccpartdisj  44900  lighneallem2  45069  lighneallem3  45070  lighneallem4  45073  proththd  45077  sgoldbeven3prm  45246  bgoldbtbndlem2  45269  upgrwlkupwlk  45313  lindslinindsimp1  45809  nn0sumshdiglemA  45976  eenglngeehlnmlem2  46095  setrec1lem4  46407