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  6344  ordelinel  6465  dif20el  8496  domunfican  9295  frind  9736  recgt1i  12140  recreclt  12142  ledivp1i  12168  nngt0  12295  nnrecgt0  12307  elnnnn0c  12577  elnnz1  12648  recnz  12700  uz3m2nn  12947  ledivge1le  13119  xrub  13368  1mod  13968  expubnd  14246  expnbnd  14300  expnlbnd  14301  hashgt23el  14493  resqrex  15341  sin02gt0  16286  oddge22np1  16445  dvdsnprmd  16786  prmlem1  17205  prmlem2  17218  lsmss2  19800  ovolicopnf  25758  voliunlem3  25786  volsup  25790  volivth  25841  itg2seq  25976  itg2monolem2  25985  reeff1olem  26689  sinq12gt0  26752  logdivlti  26865  logdivlt  26866  efexple  27525  gausslemma2dlem4  27613  axlowdimlem16  29422  axlowdimlem17  29423  axlowdim  29426  rusgr1vtx  30056  dmdbr2  32792  dfon2lem3  36370  dfon2lem7  36374  nn0prpwlem  36949  bj-resta  37854  tan2h  38374  mblfinlem4  38417  m1mod0mod1  48256  m1modmmod  48260  muldvdsfacgt  48282  muldvdsfacm1  48283  iccpartgt  48335  nprmdvdsfacm1lem4  48534  gbegt5  48685  gbowgt5  48686  sbgoldbalt  48705  sgoldbeven3prm  48707  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  evengpoap3  48723  nnsum4primesevenALTV  48725  regt1loggt0  49474  rege1logbrege0  49496  rege1logbzge0  49497