Theorem mpani 695

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 694	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  mp2ani  697  frpoind  6340  wfiOLD  6349  ordelinel  6462  dif20el  8500  domunfican  9316  frind  9741  mulgt1  12069  recgt1i  12107  recreclt  12109  ledivp1i  12135  nngt0  12239  nnrecgt0  12251  elnnnn0c  12513  elnnz1  12584  recnz  12633  uz3m2nn  12871  ledivge1le  13041  xrub  13287  1mod  13864  expubnd  14138  expnbnd  14191  expnlbnd  14192  hashgt23el  14380  resqrex  15193  sin02gt0  16131  oddge22np1  16288  dvdsnprmd  16623  prmlem1  17037  prmlem2  17049  lsmss2  19528  ovolicopnf  25023  voliunlem3  25051  volsup  25055  volivth  25106  itg2seq  25242  itg2monolem2  25251  reeff1olem  25940  sinq12gt0  25999  logdivlti  26110  logdivlt  26111  efexple  26764  gausslemma2dlem4  26852  axlowdimlem16  28195  axlowdimlem17  28196  axlowdim  28199  rusgr1vtx  28825  dmdbr2  31534  dfon2lem3  34695  dfon2lem7  34699  nn0prpwlem  35145  bj-resta  35915  tan2h  36418  mblfinlem4  36466  m1mod0mod1  45972  iccpartgt  46030  gbegt5  46364  gbowgt5  46365  sbgoldbalt  46384  sgoldbeven3prm  46386  nnsum4primesodd  46399  nnsum4primesoddALTV  46400  evengpoap3  46402  nnsum4primesevenALTV  46404  m1modmmod  47109  difmodm1lt  47110  regt1loggt0  47124  rege1logbrege0  47146  rege1logbzge0  47147