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  6345  ordelinel  6466  dif20el  8516  domunfican  9316  frind  9757  recgt1i  12217  recreclt  12219  ledivp1i  12245  nngt0  12372  nnrecgt0  12384  elnnnn0c  12654  elnnz1  12725  recnz  12777  uz3m2nn  13024  ledivge1le  13196  xrub  13445  1mod  14046  expubnd  14324  expnbnd  14379  expnlbnd  14380  hashgt23el  14572  resqrex  15422  sin02gt0  16365  oddge22np1  16524  dvdsnprmd  16870  prmlem1  17290  prmlem2  17303  lsmss2  19886  ovolicopnf  25850  voliunlem3  25878  volsup  25882  volivth  25933  itg2seq  26068  itg2monolem2  26077  reeff1olem  26778  sinq12gt0  26841  logdivlti  26953  logdivlt  26954  efexple  27613  gausslemma2dlem4  27701  axlowdimlem16  29540  axlowdimlem17  29541  axlowdim  29544  rusgr1vtx  30174  dmdbr2  32910  dfon2lem3  36639  dfon2lem7  36643  nn0prpwlem  37202  bj-resta  38109  tan2h  38628  mblfinlem4  38671  m1mod0mod1  48523  m1modmmod  48527  muldvdsfacgt  48549  muldvdsfacm1  48550  iccpartgt  48602  nprmdvdsfacm1lem4  48801  gbegt5  48952  gbowgt5  48953  sbgoldbalt  48972  sgoldbeven3prm  48974  nnsum4primesodd  48987  nnsum4primesoddALTV  48988  evengpoap3  48990  nnsum4primesevenALTV  48992  regt1loggt0  49741  rege1logbrege0  49763  rege1logbzge0  49764