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  6350  ordelinel  6471  dif20el  8499  domunfican  9291  frind  9732  recgt1i  12130  recreclt  12132  ledivp1i  12158  nngt0  12285  nnrecgt0  12297  elnnnn0c  12567  elnnz1  12638  recnz  12689  uz3m2nn  12936  ledivge1le  13107  xrub  13356  1mod  13956  expubnd  14234  expnbnd  14288  expnlbnd  14289  hashgt23el  14481  resqrex  15327  sin02gt0  16273  oddge22np1  16432  dvdsnprmd  16773  prmlem1  17192  prmlem2  17205  lsmss2  19768  ovolicopnf  25720  voliunlem3  25748  volsup  25752  volivth  25803  itg2seq  25938  itg2monolem2  25947  reeff1olem  26646  sinq12gt0  26709  logdivlti  26822  logdivlt  26823  efexple  27482  gausslemma2dlem4  27570  axlowdimlem16  29344  axlowdimlem17  29345  axlowdim  29348  rusgr1vtx  29975  dmdbr2  32692  dfon2lem3  36296  dfon2lem7  36300  nn0prpwlem  36874  bj-resta  37779  tan2h  38304  mblfinlem4  38352  m1mod0mod1  48138  m1modmmod  48142  muldvdsfacgt  48164  muldvdsfacm1  48165  iccpartgt  48217  nprmdvdsfacm1lem4  48416  gbegt5  48567  gbowgt5  48568  sbgoldbalt  48587  sgoldbeven3prm  48589  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  evengpoap3  48605  nnsum4primesevenALTV  48607  regt1loggt0  49357  rege1logbrege0  49379  rege1logbzge0  49380