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  6306  ordelinel  6426  dif20el  8440  domunfican  9232  frind  9674  mulgt1OLD  12014  recgt1i  12053  recreclt  12055  ledivp1i  12081  nngt0  12208  nnrecgt0  12220  elnnnn0c  12482  elnnz1  12553  recnz  12604  uz3m2nn  12844  ledivge1le  13015  xrub  13264  1mod  13862  expubnd  14140  expnbnd  14194  expnlbnd  14195  hashgt23el  14386  resqrex  15212  sin02gt0  16159  oddge22np1  16318  dvdsnprmd  16659  prmlem1  17078  prmlem2  17090  lsmss2  19642  ovolicopnf  25491  voliunlem3  25519  volsup  25523  volivth  25574  itg2seq  25709  itg2monolem2  25718  reeff1olem  26411  sinq12gt0  26471  logdivlti  26584  logdivlt  26585  efexple  27244  gausslemma2dlem4  27332  axlowdimlem16  29026  axlowdimlem17  29027  axlowdim  29030  rusgr1vtx  29657  dmdbr2  32374  dfon2lem3  35965  dfon2lem7  35969  nn0prpwlem  36504  bj-resta  37408  tan2h  37933  mblfinlem4  37981  m1mod0mod1  47808  m1modmmod  47812  muldvdsfacgt  47834  muldvdsfacm1  47835  iccpartgt  47887  nprmdvdsfacm1lem4  48086  gbegt5  48237  gbowgt5  48238  sbgoldbalt  48257  sgoldbeven3prm  48259  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  evengpoap3  48275  nnsum4primesevenALTV  48277  regt1loggt0  49012  rege1logbrege0  49034  rege1logbzge0  49035