Theorem mpani 696

Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpani.1	⊢ 𝜓
mpani.2	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mpani	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem mpani

Step	Hyp	Ref	Expression
1		mpani.1	. . 3 ⊢ 𝜓
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜓)
3		mpani.2	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
4	2, 3	mpand 695	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mp2ani  698  frpoind  6318  ordelinel  6438  dif20el  8472  domunfican  9279  frind  9710  mulgt1OLD  12048  recgt1i  12087  recreclt  12089  ledivp1i  12115  nngt0  12224  nnrecgt0  12236  elnnnn0c  12494  elnnz1  12566  recnz  12616  uz3m2nn  12860  ledivge1le  13031  xrub  13279  1mod  13872  expubnd  14150  expnbnd  14204  expnlbnd  14205  hashgt23el  14396  resqrex  15223  sin02gt0  16167  oddge22np1  16326  dvdsnprmd  16667  prmlem1  17085  prmlem2  17097  lsmss2  19604  ovolicopnf  25432  voliunlem3  25460  volsup  25464  volivth  25515  itg2seq  25650  itg2monolem2  25659  reeff1olem  26363  sinq12gt0  26423  logdivlti  26536  logdivlt  26537  efexple  27199  gausslemma2dlem4  27287  axlowdimlem16  28891  axlowdimlem17  28892  axlowdim  28895  rusgr1vtx  29523  dmdbr2  32239  dfon2lem3  35780  dfon2lem7  35784  nn0prpwlem  36317  bj-resta  37091  tan2h  37613  mblfinlem4  37661  m1mod0mod1  47359  m1modmmod  47363  iccpartgt  47432  gbegt5  47766  gbowgt5  47767  sbgoldbalt  47786  sgoldbeven3prm  47788  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  evengpoap3  47804  nnsum4primesevenALTV  47806  regt1loggt0  48529  rege1logbrege0  48551  rege1logbzge0  48552