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 399

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 210  df-an 400

This theorem is referenced by:  mp2ani  697  wfi  6149  ordelinel  6257  dif20el  8113  domunfican  8775  mulgt1  11488  recgt1i  11526  recreclt  11528  ledivp1i  11554  nngt0  11656  nnrecgt0  11668  elnnnn0c  11930  elnnz1  11996  recnz  12045  uz3m2nn  12279  ledivge1le  12448  xrub  12693  1mod  13266  expubnd  13537  expnbnd  13589  expnlbnd  13590  hashgt23el  13781  resqrex  14602  sin02gt0  15537  oddge22np1  15690  dvdsnprmd  16024  prmlem1  16433  prmlem2  16445  lsmss2  18785  ovolicopnf  24128  voliunlem3  24156  volsup  24160  volivth  24211  itg2seq  24346  itg2monolem2  24355  reeff1olem  25041  sinq12gt0  25100  logdivlti  25211  logdivlt  25212  efexple  25865  gausslemma2dlem4  25953  axlowdimlem16  26751  axlowdimlem17  26752  axlowdim  26755  rusgr1vtx  27378  dmdbr2  30086  dfon2lem3  33143  dfon2lem7  33147  frpoind  33193  frind  33198  nn0prpwlem  33783  bj-resta  34511  tan2h  35049  mblfinlem4  35097  m1mod0mod1  43886  iccpartgt  43944  gbegt5  44279  gbowgt5  44280  sbgoldbalt  44299  sgoldbeven3prm  44301  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  evengpoap3  44317  nnsum4primesevenALTV  44319  m1modmmod  44935  difmodm1lt  44936  regt1loggt0  44950  rege1logbrege0  44972  rege1logbzge0  44973