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  6294  ordelinel  6414  dif20el  8430  domunfican  9230  frind  9665  mulgt1OLD  12001  recgt1i  12040  recreclt  12042  ledivp1i  12068  nngt0  12177  nnrecgt0  12189  elnnnn0c  12447  elnnz1  12519  recnz  12569  uz3m2nn  12813  ledivge1le  12984  xrub  13232  1mod  13825  expubnd  14103  expnbnd  14157  expnlbnd  14158  hashgt23el  14349  resqrex  15175  sin02gt0  16119  oddge22np1  16278  dvdsnprmd  16619  prmlem1  17037  prmlem2  17049  lsmss2  19564  ovolicopnf  25441  voliunlem3  25469  volsup  25473  volivth  25524  itg2seq  25659  itg2monolem2  25668  reeff1olem  26372  sinq12gt0  26432  logdivlti  26545  logdivlt  26546  efexple  27208  gausslemma2dlem4  27296  axlowdimlem16  28920  axlowdimlem17  28921  axlowdim  28924  rusgr1vtx  29552  dmdbr2  32265  dfon2lem3  35758  dfon2lem7  35762  nn0prpwlem  36295  bj-resta  37069  tan2h  37591  mblfinlem4  37639  m1mod0mod1  47339  m1modmmod  47343  iccpartgt  47412  gbegt5  47746  gbowgt5  47747  sbgoldbalt  47766  sgoldbeven3prm  47768  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  evengpoap3  47784  nnsum4primesevenALTV  47786  regt1loggt0  48522  rege1logbrege0  48544  rege1logbzge0  48545