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  rspcimdv  3602  riotass2  7395  peano5  7883  peano5OLD  7884  oeordi  8586  isf34lem4  10371  domtriomlem  10436  axcclem  10451  ssnn0fi  13949  repswrevw  14736  rlimcn1  15531  climcn1  15535  climcn2  15536  dvdsgcd  16485  lcmfunsnlem2lem1  16574  coprmgcdb  16585  nprm  16624  pcqmul  16785  prmgaplem7  16989  lubun  18467  grpid  18859  psgnunilem4  19364  gexdvds  19451  scmate  22011  cayleyhamilton1  22393  uniopn  22398  tgcmp  22904  uncmp  22906  nconnsubb  22926  comppfsc  23035  kgencn2  23060  isufil2  23411  cfinufil  23431  fin1aufil  23435  flimopn  23478  cnpflf  23504  flimfnfcls  23531  fcfnei  23538  metcnp3  24048  cncfco  24422  ellimc3  25395  dvfsumrlim  25547  cxploglim  26479  2sqreultblem  26948  nbuhgr2vtx1edgblem  28605  nbusgrvtxm1  28633  wlkp1lem6  28932  pthdlem2lem  29021  crctcshwlkn0lem4  29064  crctcshwlkn0lem5  29065  wlknwwlksnbij  29139  eupth2  29489  frgrncvvdeqlem8  29556  grpoid  29768  blocnilem  30052  htthlem  30165  nmcexi  31274  dmdbr3  31553  dmdbr4  31554  atom1d  31601  mclsax  34555  dfon2lem8  34757  nn0prpwlem  35202  bj-ceqsalt0  35759  bj-ceqsalt1  35760  filbcmb  36603  divrngidl  36891  lshpcmp  37853  lsat0cv  37898  atnle  38182  lpolconN  40353  ss2iundf  42400  iccpartdisj  46095  lighneallem2  46264  lighneallem3  46265  lighneallem4  46268  proththd  46272  sgoldbeven3prm  46441  bgoldbtbndlem2  46464  upgrwlkupwlk  46508  rngqiprngfulem2  46787  rngqipring1  46791  lindslinindsimp1  47128  nn0sumshdiglemA  47295  eenglngeehlnmlem2  47414  setrec1lem4  47725