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 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  697  frpoind  6374  wfiOLD  6383  ordelinel  6496  dif20el  8561  domunfican  9389  frind  9819  mulgt1OLD  12153  recgt1i  12192  recreclt  12194  ledivp1i  12220  nngt0  12324  nnrecgt0  12336  elnnnn0c  12598  elnnz1  12669  recnz  12718  uz3m2nn  12956  ledivge1le  13128  xrub  13374  1mod  13954  expubnd  14227  expnbnd  14281  expnlbnd  14282  hashgt23el  14473  resqrex  15299  sin02gt0  16240  oddge22np1  16397  dvdsnprmd  16737  prmlem1  17155  prmlem2  17167  lsmss2  19709  ovolicopnf  25578  voliunlem3  25606  volsup  25610  volivth  25661  itg2seq  25797  itg2monolem2  25806  reeff1olem  26508  sinq12gt0  26567  logdivlti  26680  logdivlt  26681  efexple  27343  gausslemma2dlem4  27431  axlowdimlem16  28990  axlowdimlem17  28991  axlowdim  28994  rusgr1vtx  29624  dmdbr2  32335  dfon2lem3  35749  dfon2lem7  35753  nn0prpwlem  36288  bj-resta  37062  tan2h  37572  mblfinlem4  37620  m1mod0mod1  47243  iccpartgt  47301  gbegt5  47635  gbowgt5  47636  sbgoldbalt  47655  sgoldbeven3prm  47657  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  evengpoap3  47673  nnsum4primesevenALTV  47675  m1modmmod  48255  difmodm1lt  48256  regt1loggt0  48270  rege1logbrege0  48292  rege1logbzge0  48293