Theorem mpani 693

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 692	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 206  df-an 397

This theorem is referenced by:  mp2ani  695  frpoind  6245  wfiOLD  6254  ordelinel  6364  dif20el  8335  domunfican  9087  frind  9508  mulgt1  11834  recgt1i  11872  recreclt  11874  ledivp1i  11900  nngt0  12004  nnrecgt0  12016  elnnnn0c  12278  elnnz1  12346  recnz  12395  uz3m2nn  12631  ledivge1le  12801  xrub  13046  1mod  13623  expubnd  13895  expnbnd  13947  expnlbnd  13948  hashgt23el  14139  resqrex  14962  sin02gt0  15901  oddge22np1  16058  dvdsnprmd  16395  prmlem1  16809  prmlem2  16821  lsmss2  19273  ovolicopnf  24688  voliunlem3  24716  volsup  24720  volivth  24771  itg2seq  24907  itg2monolem2  24916  reeff1olem  25605  sinq12gt0  25664  logdivlti  25775  logdivlt  25776  efexple  26429  gausslemma2dlem4  26517  axlowdimlem16  27325  axlowdimlem17  27326  axlowdim  27329  rusgr1vtx  27955  dmdbr2  30665  dfon2lem3  33761  dfon2lem7  33765  nn0prpwlem  34511  bj-resta  35267  tan2h  35769  mblfinlem4  35817  m1mod0mod1  44821  iccpartgt  44879  gbegt5  45213  gbowgt5  45214  sbgoldbalt  45233  sgoldbeven3prm  45235  nnsum4primesodd  45248  nnsum4primesoddALTV  45249  evengpoap3  45251  nnsum4primesevenALTV  45253  m1modmmod  45867  difmodm1lt  45868  regt1loggt0  45882  rege1logbrege0  45904  rege1logbzge0  45905