Theorem mpani 706

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mp2ani  708  frpoind  6325  ordelinel  6445  dif20el  8469  domunfican  9262  frind  9705  mulgt1OLD  12047  recgt1i  12086  recreclt  12088  ledivp1i  12114  nngt0  12241  nnrecgt0  12253  elnnnn0c  12523  elnnz1  12594  recnz  12645  uz3m2nn  12892  ledivge1le  13063  xrub  13312  1mod  13910  expubnd  14188  expnbnd  14242  expnlbnd  14243  hashgt23el  14434  resqrex  15260  sin02gt0  16207  oddge22np1  16366  dvdsnprmd  16707  prmlem1  17126  prmlem2  17139  lsmss2  19690  ovolicopnf  25566  voliunlem3  25594  volsup  25598  volivth  25649  itg2seq  25784  itg2monolem2  25793  reeff1olem  26486  sinq12gt0  26549  logdivlti  26662  logdivlt  26663  efexple  27322  gausslemma2dlem4  27410  axlowdimlem16  29104  axlowdimlem17  29105  axlowdim  29108  rusgr1vtx  29735  dmdbr2  32452  dfon2lem3  36097  dfon2lem7  36101  nn0prpwlem  36646  bj-resta  37550  tan2h  38075  mblfinlem4  38123  m1mod0mod1  47918  m1modmmod  47922  muldvdsfacgt  47944  muldvdsfacm1  47945  iccpartgt  47997  nprmdvdsfacm1lem4  48196  gbegt5  48347  gbowgt5  48348  sbgoldbalt  48367  sgoldbeven3prm  48369  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  evengpoap3  48385  nnsum4primesevenALTV  48387  regt1loggt0  49122  rege1logbrege0  49144  rege1logbzge0  49145