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  6315  ordelinel  6435  dif20el  8469  domunfican  9272  frind  9703  mulgt1OLD  12041  recgt1i  12080  recreclt  12082  ledivp1i  12108  nngt0  12217  nnrecgt0  12229  elnnnn0c  12487  elnnz1  12559  recnz  12609  uz3m2nn  12853  ledivge1le  13024  xrub  13272  1mod  13865  expubnd  14143  expnbnd  14197  expnlbnd  14198  hashgt23el  14389  resqrex  15216  sin02gt0  16160  oddge22np1  16319  dvdsnprmd  16660  prmlem1  17078  prmlem2  17090  lsmss2  19597  ovolicopnf  25425  voliunlem3  25453  volsup  25457  volivth  25508  itg2seq  25643  itg2monolem2  25652  reeff1olem  26356  sinq12gt0  26416  logdivlti  26529  logdivlt  26530  efexple  27192  gausslemma2dlem4  27280  axlowdimlem16  28884  axlowdimlem17  28885  axlowdim  28888  rusgr1vtx  29516  dmdbr2  32232  dfon2lem3  35773  dfon2lem7  35777  nn0prpwlem  36310  bj-resta  37084  tan2h  37606  mblfinlem4  37654  m1mod0mod1  47355  m1modmmod  47359  iccpartgt  47428  gbegt5  47762  gbowgt5  47763  sbgoldbalt  47782  sgoldbeven3prm  47784  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  evengpoap3  47800  nnsum4primesevenALTV  47802  regt1loggt0  48525  rege1logbrege0  48547  rege1logbzge0  48548