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  6363  wfiOLD  6372  ordelinel  6485  dif20el  8543  domunfican  9361  frind  9790  mulgt1OLD  12126  recgt1i  12165  recreclt  12167  ledivp1i  12193  nngt0  12297  nnrecgt0  12309  elnnnn0c  12571  elnnz1  12643  recnz  12693  uz3m2nn  12933  ledivge1le  13106  xrub  13354  1mod  13943  expubnd  14217  expnbnd  14271  expnlbnd  14272  hashgt23el  14463  resqrex  15289  sin02gt0  16228  oddge22np1  16386  dvdsnprmd  16727  prmlem1  17145  prmlem2  17157  lsmss2  19685  ovolicopnf  25559  voliunlem3  25587  volsup  25591  volivth  25642  itg2seq  25777  itg2monolem2  25786  reeff1olem  26490  sinq12gt0  26549  logdivlti  26662  logdivlt  26663  efexple  27325  gausslemma2dlem4  27413  axlowdimlem16  28972  axlowdimlem17  28973  axlowdim  28976  rusgr1vtx  29606  dmdbr2  32322  dfon2lem3  35786  dfon2lem7  35790  nn0prpwlem  36323  bj-resta  37097  tan2h  37619  mblfinlem4  37667  m1mod0mod1  47356  iccpartgt  47414  gbegt5  47748  gbowgt5  47749  sbgoldbalt  47768  sgoldbeven3prm  47770  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  evengpoap3  47786  nnsum4primesevenALTV  47788  m1modmmod  48442  difmodm1lt  48443  regt1loggt0  48457  rege1logbrege0  48479  rege1logbzge0  48480