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  6300  ordelinel  6420  dif20el  8433  domunfican  9225  frind  9665  mulgt1OLD  12005  recgt1i  12044  recreclt  12046  ledivp1i  12072  nngt0  12199  nnrecgt0  12211  elnnnn0c  12473  elnnz1  12544  recnz  12595  uz3m2nn  12835  ledivge1le  13006  xrub  13255  1mod  13853  expubnd  14131  expnbnd  14185  expnlbnd  14186  hashgt23el  14377  resqrex  15203  sin02gt0  16150  oddge22np1  16309  dvdsnprmd  16650  prmlem1  17069  prmlem2  17081  lsmss2  19633  ovolicopnf  25501  voliunlem3  25529  volsup  25533  volivth  25584  itg2seq  25719  itg2monolem2  25728  reeff1olem  26424  sinq12gt0  26484  logdivlti  26597  logdivlt  26598  efexple  27258  gausslemma2dlem4  27346  axlowdimlem16  29040  axlowdimlem17  29041  axlowdim  29044  rusgr1vtx  29672  dmdbr2  32389  dfon2lem3  35981  dfon2lem7  35985  nn0prpwlem  36520  bj-resta  37424  tan2h  37947  mblfinlem4  37995  m1mod0mod1  47820  m1modmmod  47824  muldvdsfacgt  47846  muldvdsfacm1  47847  iccpartgt  47899  nprmdvdsfacm1lem4  48098  gbegt5  48249  gbowgt5  48250  sbgoldbalt  48269  sgoldbeven3prm  48271  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  evengpoap3  48287  nnsum4primesevenALTV  48289  regt1loggt0  49024  rege1logbrege0  49046  rege1logbzge0  49047