Theorem mpani 702

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mp2ani  704  frpoind  6300  ordelinel  6420  dif20el  8437  domunfican  9229  frind  9672  mulgt1OLD  12012  recgt1i  12051  recreclt  12053  ledivp1i  12079  nngt0  12206  nnrecgt0  12218  elnnnn0c  12480  elnnz1  12551  recnz  12602  uz3m2nn  12842  ledivge1le  13013  xrub  13262  1mod  13860  expubnd  14138  expnbnd  14192  expnlbnd  14193  hashgt23el  14384  resqrex  15210  sin02gt0  16157  oddge22np1  16316  dvdsnprmd  16657  prmlem1  17076  prmlem2  17088  lsmss2  19640  ovolicopnf  25516  voliunlem3  25544  volsup  25548  volivth  25599  itg2seq  25734  itg2monolem2  25743  reeff1olem  26436  sinq12gt0  26496  logdivlti  26609  logdivlt  26610  efexple  27269  gausslemma2dlem4  27357  axlowdimlem16  29051  axlowdimlem17  29052  axlowdim  29055  rusgr1vtx  29682  dmdbr2  32399  dfon2lem3  36018  dfon2lem7  36022  nn0prpwlem  36557  bj-resta  37461  tan2h  37986  mblfinlem4  38034  m1mod0mod1  47830  m1modmmod  47834  muldvdsfacgt  47856  muldvdsfacm1  47857  iccpartgt  47909  nprmdvdsfacm1lem4  48108  gbegt5  48259  gbowgt5  48260  sbgoldbalt  48279  sgoldbeven3prm  48281  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  evengpoap3  48297  nnsum4primesevenALTV  48299  regt1loggt0  49034  rege1logbrege0  49056  rege1logbzge0  49057