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  3563  riotass2  7339  peano5  7829  oeordi  8508  isf34lem4  10275  domtriomlem  10340  axcclem  10355  ssnn0fi  13894  repswrevw  14696  rlimcn1  15497  climcn1  15501  climcn2  15502  dvdsgcd  16457  lcmfunsnlem2lem1  16551  coprmgcdb  16562  nprm  16601  pcqmul  16767  prmgaplem7  16971  lubun  18423  grpid  18890  psgnunilem4  19411  gexdvds  19498  rngqiprngfulem2  21251  rngqipring1  21255  scmate  22426  cayleyhamilton1  22808  uniopn  22813  tgcmp  23317  uncmp  23319  nconnsubb  23339  comppfsc  23448  kgencn2  23473  isufil2  23824  cfinufil  23844  fin1aufil  23848  flimopn  23891  cnpflf  23917  flimfnfcls  23944  fcfnei  23951  metcnp3  24456  cncfco  24828  ellimc3  25808  dvfsumrlim  25966  cxploglim  26916  2sqreultblem  27387  nbuhgr2vtx1edgblem  29331  nbusgrvtxm1  29359  wlkp1lem6  29657  pthdlem2lem  29747  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  wlknwwlksnbij  29868  eupth2  30221  frgrncvvdeqlem8  30288  grpoid  30502  blocnilem  30786  htthlem  30899  nmcexi  32008  dmdbr3  32287  dmdbr4  32288  atom1d  32335  dvelimalcased  35108  dvelimexcased  35110  mclsax  35634  dfon2lem8  35853  nn0prpwlem  36387  bj-ceqsalt0  36949  bj-ceqsalt1  36950  filbcmb  37801  divrngidl  38089  lshpcmp  39108  lsat0cv  39153  atnle  39437  lpolconN  41607  ss2iundf  43777  iccpartdisj  47562  lighneallem2  47731  lighneallem3  47732  lighneallem4  47735  proththd  47739  sgoldbeven3prm  47908  bgoldbtbndlem2  47931  upgrimwlklem5  48026  upgrwlkupwlk  48265  lindslinindsimp1  48583  nn0sumshdiglemA  48745  eenglngeehlnmlem2  48864  setrec1lem4  49816