Theorem mpani 708

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  mp2ani  710  frpoind  6345  ordelinel  6466  dif20el  8491  domunfican  9282  frind  9723  recgt1i  12113  recreclt  12115  ledivp1i  12141  nngt0  12268  nnrecgt0  12280  elnnnn0c  12550  elnnz1  12621  recnz  12672  uz3m2nn  12919  ledivge1le  13090  xrub  13339  1mod  13938  expubnd  14216  expnbnd  14270  expnlbnd  14271  hashgt23el  14463  resqrex  15303  sin02gt0  16249  oddge22np1  16408  dvdsnprmd  16749  prmlem1  17168  prmlem2  17181  lsmss2  19738  ovolicopnf  25664  voliunlem3  25692  volsup  25696  volivth  25747  itg2seq  25882  itg2monolem2  25891  reeff1olem  26587  sinq12gt0  26650  logdivlti  26763  logdivlt  26764  efexple  27423  gausslemma2dlem4  27511  axlowdimlem16  29285  axlowdimlem17  29286  axlowdim  29289  rusgr1vtx  29916  dmdbr2  32633  dfon2lem3  36253  dfon2lem7  36257  nn0prpwlem  36811  bj-resta  37716  tan2h  38241  mblfinlem4  38289  m1mod0mod1  48074  m1modmmod  48078  muldvdsfacgt  48100  muldvdsfacm1  48101  iccpartgt  48153  nprmdvdsfacm1lem4  48352  gbegt5  48503  gbowgt5  48504  sbgoldbalt  48523  sgoldbeven3prm  48525  nnsum4primesodd  48538  nnsum4primesoddALTV  48539  evengpoap3  48541  nnsum4primesevenALTV  48543  regt1loggt0  49293  rege1logbrege0  49315  rege1logbzge0  49316