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  6294  ordelinel  6414  dif20el  8426  domunfican  9213  frind  9650  mulgt1OLD  11987  recgt1i  12026  recreclt  12028  ledivp1i  12054  nngt0  12163  nnrecgt0  12175  elnnnn0c  12433  elnnz1  12504  recnz  12554  uz3m2nn  12794  ledivge1le  12965  xrub  13213  1mod  13809  expubnd  14087  expnbnd  14141  expnlbnd  14142  hashgt23el  14333  resqrex  15159  sin02gt0  16103  oddge22np1  16262  dvdsnprmd  16603  prmlem1  17021  prmlem2  17033  lsmss2  19581  ovolicopnf  25453  voliunlem3  25481  volsup  25485  volivth  25536  itg2seq  25671  itg2monolem2  25680  reeff1olem  26384  sinq12gt0  26444  logdivlti  26557  logdivlt  26558  efexple  27220  gausslemma2dlem4  27308  axlowdimlem16  28937  axlowdimlem17  28938  axlowdim  28941  rusgr1vtx  29569  dmdbr2  32285  dfon2lem3  35848  dfon2lem7  35852  nn0prpwlem  36387  bj-resta  37161  tan2h  37672  mblfinlem4  37720  m1mod0mod1  47478  m1modmmod  47482  iccpartgt  47551  gbegt5  47885  gbowgt5  47886  sbgoldbalt  47905  sgoldbeven3prm  47907  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  evengpoap3  47923  nnsum4primesevenALTV  47925  regt1loggt0  48661  rege1logbrege0  48683  rege1logbzge0  48684