Theorem mpani 689

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  mp2ani  691  wfi  5954  ordelinel  6062  dif20el  7853  domunfican  8503  mulgt1  11213  recgt1i  11251  recreclt  11253  ledivp1i  11280  nngt0  11384  nnrecgt0  11395  elnnnn0c  11666  elnnz1  11732  recnz  11781  uz3m2nn  12014  ledivge1le  12186  xrub  12431  1mod  12998  expubnd  13216  expnbnd  13288  expnlbnd  13289  pfx2  14069  resqrex  14369  sin02gt0  15295  oddge22np1  15448  dvdsnprmd  15776  prmlem1  16181  prmlem2  16193  lsmss2  18433  ovolicopnf  23691  voliunlem3  23719  volsup  23723  volivth  23774  itg2seq  23909  itg2monolem2  23918  reeff1olem  24600  sinq12gt0  24660  logdivlti  24766  logdivlt  24767  efexple  25420  gausslemma2dlem4  25508  axlowdimlem16  26257  axlowdimlem17  26258  axlowdim  26261  rusgr1vtx  26887  dmdbr2  29718  dfon2lem3  32229  dfon2lem7  32233  frpoind  32280  frind  32283  nn0prpwlem  32856  bj-resta  33573  tan2h  33945  mblfinlem4  33994  m1mod0mod1  42228  iccpartgt  42252  gbegt5  42480  gbowgt5  42481  sbgoldbalt  42500  sgoldbeven3prm  42502  nnsum4primesodd  42515  nnsum4primesoddALTV  42516  evengpoap3  42518  nnsum4primesevenALTV  42520  m1modmmod  43164  difmodm1lt  43165  regt1loggt0  43178  rege1logbrege0  43200  rege1logbzge0  43201