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  6289  ordelinel  6409  dif20el  8420  domunfican  9206  frind  9640  mulgt1OLD  11977  recgt1i  12016  recreclt  12018  ledivp1i  12044  nngt0  12153  nnrecgt0  12165  elnnnn0c  12423  elnnz1  12495  recnz  12545  uz3m2nn  12789  ledivge1le  12960  xrub  13208  1mod  13804  expubnd  14082  expnbnd  14136  expnlbnd  14137  hashgt23el  14328  resqrex  15154  sin02gt0  16098  oddge22np1  16257  dvdsnprmd  16598  prmlem1  17016  prmlem2  17028  lsmss2  19577  ovolicopnf  25450  voliunlem3  25478  volsup  25482  volivth  25533  itg2seq  25668  itg2monolem2  25677  reeff1olem  26381  sinq12gt0  26441  logdivlti  26554  logdivlt  26555  efexple  27217  gausslemma2dlem4  27305  axlowdimlem16  28933  axlowdimlem17  28934  axlowdim  28937  rusgr1vtx  29565  dmdbr2  32278  dfon2lem3  35818  dfon2lem7  35822  nn0prpwlem  36355  bj-resta  37129  tan2h  37651  mblfinlem4  37699  m1mod0mod1  47384  m1modmmod  47388  iccpartgt  47457  gbegt5  47791  gbowgt5  47792  sbgoldbalt  47811  sgoldbeven3prm  47813  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  evengpoap3  47829  nnsum4primesevenALTV  47831  regt1loggt0  48567  rege1logbrege0  48589  rege1logbzge0  48590