Theorem mpani 708

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mp2ani  710  wfi  5630  ordelinel  5742  ordelinelOLD  5743  dif20el  7472  domunfican  8118  mulgt1  10761  recgt1i  10799  recreclt  10801  ledivp1i  10828  nngt0  10926  nnrecgt0  10935  elnnnn0c  11215  elnnz1  11280  recnz  11328  uz3m2nn  11607  ledivge1le  11777  xrub  12014  1mod  12564  expubnd  12783  expnbnd  12855  expnlbnd  12856  resqrex  13839  sin02gt0  14761  oddge22np1  14911  dvdsnprmd  15241  prmlem1  15652  prmlem2  15665  lsmss2  17904  ovolicopnf  23099  voliunlem3  23127  volsup  23131  volivth  23181  itg2seq  23315  itg2monolem2  23324  reeff1olem  24004  sinq12gt0  24063  logdivlti  24170  logdivlt  24171  efexple  24806  gausslemma2dlem4  24894  axlowdimlem16  25637  axlowdimlem17  25638  axlowdim  25641  dmdbr2  28546  dfon2lem3  30934  dfon2lem7  30938  frind  30984  nn0prpwlem  31487  bj-resta  32230  tan2h  32571  mblfinlem4  32619  m1mod0mod1  39949  iccpartgt  39965  gbegt5  40183  gbogt5  40184  sgoldbalt  40203  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  evengpoap3  40215  nnsum4primesevenALTV  40217  pfx2  40275  rusgr1vtx  40788  frgrwopreglem2  41482  m1modmmod  42110  difmodm1lt  42111  regt1loggt0  42128  rege1logbrege0  42150  rege1logbzge0  42151