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  6331  wfiOLD  6340  ordelinel  6455  dif20el  8517  domunfican  9333  frind  9764  mulgt1OLD  12100  recgt1i  12139  recreclt  12141  ledivp1i  12167  nngt0  12271  nnrecgt0  12283  elnnnn0c  12546  elnnz1  12618  recnz  12668  uz3m2nn  12907  ledivge1le  13080  xrub  13328  1mod  13920  expubnd  14196  expnbnd  14250  expnlbnd  14251  hashgt23el  14442  resqrex  15269  sin02gt0  16210  oddge22np1  16368  dvdsnprmd  16709  prmlem1  17127  prmlem2  17139  lsmss2  19648  ovolicopnf  25477  voliunlem3  25505  volsup  25509  volivth  25560  itg2seq  25695  itg2monolem2  25704  reeff1olem  26408  sinq12gt0  26468  logdivlti  26581  logdivlt  26582  efexple  27244  gausslemma2dlem4  27332  axlowdimlem16  28936  axlowdimlem17  28937  axlowdim  28940  rusgr1vtx  29568  dmdbr2  32284  dfon2lem3  35803  dfon2lem7  35807  nn0prpwlem  36340  bj-resta  37114  tan2h  37636  mblfinlem4  37684  m1mod0mod1  47383  iccpartgt  47441  gbegt5  47775  gbowgt5  47776  sbgoldbalt  47795  sgoldbeven3prm  47797  nnsum4primesodd  47810  nnsum4primesoddALTV  47811  evengpoap3  47813  nnsum4primesevenALTV  47815  m1modmmod  48501  difmodm1lt  48502  regt1loggt0  48516  rege1logbrege0  48538  rege1logbzge0  48539