Theorem mpani 709

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mp2ani  711  frpoind  6363  ordelinel  6484  dif20el  8541  domunfican  9341  frind  9781  recgt1i  12241  recreclt  12243  ledivp1i  12269  nngt0  12396  nnrecgt0  12408  elnnnn0c  12678  elnnz1  12749  recnz  12801  uz3m2nn  13048  ledivge1le  13220  xrub  13469  1mod  14070  expubnd  14348  expnbnd  14403  expnlbnd  14404  hashgt23el  14596  resqrex  15446  sin02gt0  16389  oddge22np1  16548  dvdsnprmd  16894  prmlem1  17314  prmlem2  17327  lsmss2  19911  ovolicopnf  25875  voliunlem3  25903  volsup  25907  volivth  25958  itg2seq  26093  itg2monolem2  26102  reeff1olem  26803  sinq12gt0  26866  logdivlti  26978  logdivlt  26979  efexple  27638  gausslemma2dlem4  27726  axlowdimlem16  29565  axlowdimlem17  29566  axlowdim  29569  rusgr1vtx  30199  dmdbr2  32935  k3n0j0lt  36020  k3n0k1lt  36023  k3n0k2lt  36024  dfon2lem3  36725  dfon2lem7  36729  nn0prpwlem  37288  bj-resta  38208  tan2h  38727  mblfinlem4  38770  m1mod0mod1  48635  m1modmmod  48639  muldvdsfacgt  48661  muldvdsfacm1  48662  iccpartgt  48714  nprmdvdsfacm1lem4  48913  gbegt5  49064  gbowgt5  49065  sbgoldbalt  49084  sgoldbeven3prm  49086  nnsum4primesodd  49099  nnsum4primesoddALTV  49100  evengpoap3  49102  nnsum4primesevenALTV  49104  regt1loggt0  49853  rege1logbrege0  49875  rege1logbzge0  49876