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  6364  wfiOLD  6373  ordelinel  6486  dif20el  8541  domunfican  9358  frind  9787  mulgt1OLD  12123  recgt1i  12162  recreclt  12164  ledivp1i  12190  nngt0  12294  nnrecgt0  12306  elnnnn0c  12568  elnnz1  12640  recnz  12690  uz3m2nn  12930  ledivge1le  13103  xrub  13350  1mod  13939  expubnd  14213  expnbnd  14267  expnlbnd  14268  hashgt23el  14459  resqrex  15285  sin02gt0  16224  oddge22np1  16382  dvdsnprmd  16723  prmlem1  17141  prmlem2  17153  lsmss2  19699  ovolicopnf  25572  voliunlem3  25600  volsup  25604  volivth  25655  itg2seq  25791  itg2monolem2  25800  reeff1olem  26504  sinq12gt0  26563  logdivlti  26676  logdivlt  26677  efexple  27339  gausslemma2dlem4  27427  axlowdimlem16  28986  axlowdimlem17  28987  axlowdim  28990  rusgr1vtx  29620  dmdbr2  32331  dfon2lem3  35766  dfon2lem7  35770  nn0prpwlem  36304  bj-resta  37078  tan2h  37598  mblfinlem4  37646  m1mod0mod1  47293  iccpartgt  47351  gbegt5  47685  gbowgt5  47686  sbgoldbalt  47705  sgoldbeven3prm  47707  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  evengpoap3  47723  nnsum4primesevenALTV  47725  m1modmmod  48370  difmodm1lt  48371  regt1loggt0  48385  rege1logbrege0  48407  rege1logbzge0  48408