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  6300  ordelinel  6420  dif20el  8432  domunfican  9222  frind  9662  mulgt1OLD  12000  recgt1i  12039  recreclt  12041  ledivp1i  12067  nngt0  12176  nnrecgt0  12188  elnnnn0c  12446  elnnz1  12517  recnz  12567  uz3m2nn  12807  ledivge1le  12978  xrub  13227  1mod  13823  expubnd  14101  expnbnd  14155  expnlbnd  14156  hashgt23el  14347  resqrex  15173  sin02gt0  16117  oddge22np1  16276  dvdsnprmd  16617  prmlem1  17035  prmlem2  17047  lsmss2  19596  ovolicopnf  25481  voliunlem3  25509  volsup  25513  volivth  25564  itg2seq  25699  itg2monolem2  25708  reeff1olem  26412  sinq12gt0  26472  logdivlti  26585  logdivlt  26586  efexple  27248  gausslemma2dlem4  27336  axlowdimlem16  29030  axlowdimlem17  29031  axlowdim  29034  rusgr1vtx  29662  dmdbr2  32378  dfon2lem3  35977  dfon2lem7  35981  nn0prpwlem  36516  bj-resta  37297  tan2h  37809  mblfinlem4  37857  m1mod0mod1  47596  m1modmmod  47600  iccpartgt  47669  gbegt5  48003  gbowgt5  48004  sbgoldbalt  48023  sgoldbeven3prm  48025  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  evengpoap3  48041  nnsum4primesevenALTV  48043  regt1loggt0  48778  rege1logbrege0  48800  rege1logbzge0  48801