Theorem mpani 704

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mp2ani  706  frpoind  6314  ordelinel  6434  dif20el  8458  domunfican  9251  frind  9694  mulgt1OLD  12036  recgt1i  12075  recreclt  12077  ledivp1i  12103  nngt0  12230  nnrecgt0  12242  elnnnn0c  12512  elnnz1  12583  recnz  12634  uz3m2nn  12881  ledivge1le  13052  xrub  13301  1mod  13899  expubnd  14177  expnbnd  14231  expnlbnd  14232  hashgt23el  14423  resqrex  15249  sin02gt0  16196  oddge22np1  16355  dvdsnprmd  16696  prmlem1  17115  prmlem2  17128  lsmss2  19679  ovolicopnf  25555  voliunlem3  25583  volsup  25587  volivth  25638  itg2seq  25773  itg2monolem2  25782  reeff1olem  26475  sinq12gt0  26538  logdivlti  26651  logdivlt  26652  efexple  27311  gausslemma2dlem4  27399  axlowdimlem16  29093  axlowdimlem17  29094  axlowdim  29097  rusgr1vtx  29724  dmdbr2  32441  dfon2lem3  36071  dfon2lem7  36075  nn0prpwlem  36620  bj-resta  37524  tan2h  38049  mblfinlem4  38097  m1mod0mod1  47892  m1modmmod  47896  muldvdsfacgt  47918  muldvdsfacm1  47919  iccpartgt  47971  nprmdvdsfacm1lem4  48170  gbegt5  48321  gbowgt5  48322  sbgoldbalt  48341  sgoldbeven3prm  48343  nnsum4primesodd  48356  nnsum4primesoddALTV  48357  evengpoap3  48359  nnsum4primesevenALTV  48361  regt1loggt0  49096  rege1logbrege0  49118  rege1logbzge0  49119