Theorem mpani 692

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

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  mp2ani  694  frpoind  6230  wfiOLD  6239  ordelinel  6349  dif20el  8297  domunfican  9017  frind  9439  mulgt1  11764  recgt1i  11802  recreclt  11804  ledivp1i  11830  nngt0  11934  nnrecgt0  11946  elnnnn0c  12208  elnnz1  12276  recnz  12325  uz3m2nn  12560  ledivge1le  12730  xrub  12975  1mod  13551  expubnd  13823  expnbnd  13875  expnlbnd  13876  hashgt23el  14067  resqrex  14890  sin02gt0  15829  oddge22np1  15986  dvdsnprmd  16323  prmlem1  16737  prmlem2  16749  lsmss2  19188  ovolicopnf  24593  voliunlem3  24621  volsup  24625  volivth  24676  itg2seq  24812  itg2monolem2  24821  reeff1olem  25510  sinq12gt0  25569  logdivlti  25680  logdivlt  25681  efexple  26334  gausslemma2dlem4  26422  axlowdimlem16  27228  axlowdimlem17  27229  axlowdim  27232  rusgr1vtx  27858  dmdbr2  30566  dfon2lem3  33667  dfon2lem7  33671  nn0prpwlem  34438  bj-resta  35194  tan2h  35696  mblfinlem4  35744  m1mod0mod1  44709  iccpartgt  44767  gbegt5  45101  gbowgt5  45102  sbgoldbalt  45121  sgoldbeven3prm  45123  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  evengpoap3  45139  nnsum4primesevenALTV  45141  m1modmmod  45755  difmodm1lt  45756  regt1loggt0  45770  rege1logbrege0  45792  rege1logbzge0  45793