Theorem mpani 697

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 696	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  699  frpoind  6308  ordelinel  6428  dif20el  8442  domunfican  9234  frind  9674  mulgt1OLD  12012  recgt1i  12051  recreclt  12053  ledivp1i  12079  nngt0  12188  nnrecgt0  12200  elnnnn0c  12458  elnnz1  12529  recnz  12579  uz3m2nn  12819  ledivge1le  12990  xrub  13239  1mod  13835  expubnd  14113  expnbnd  14167  expnlbnd  14168  hashgt23el  14359  resqrex  15185  sin02gt0  16129  oddge22np1  16288  dvdsnprmd  16629  prmlem1  17047  prmlem2  17059  lsmss2  19608  ovolicopnf  25493  voliunlem3  25521  volsup  25525  volivth  25576  itg2seq  25711  itg2monolem2  25720  reeff1olem  26424  sinq12gt0  26484  logdivlti  26597  logdivlt  26598  efexple  27260  gausslemma2dlem4  27348  axlowdimlem16  29042  axlowdimlem17  29043  axlowdim  29046  rusgr1vtx  29674  dmdbr2  32390  dfon2lem3  35996  dfon2lem7  36000  nn0prpwlem  36535  bj-resta  37343  tan2h  37857  mblfinlem4  37905  m1mod0mod1  47708  m1modmmod  47712  iccpartgt  47781  gbegt5  48115  gbowgt5  48116  sbgoldbalt  48135  sgoldbeven3prm  48137  nnsum4primesodd  48150  nnsum4primesoddALTV  48151  evengpoap3  48153  nnsum4primesevenALTV  48155  regt1loggt0  48890  rege1logbrege0  48912  rege1logbzge0  48913