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 400

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 210  df-an 401

This theorem is referenced by:  mp2ani  710  frpoind  6333  ordelinel  6453  dif20el  8478  domunfican  9269  frind  9710  recgt1i  12103  recreclt  12105  ledivp1i  12131  nngt0  12258  nnrecgt0  12270  elnnnn0c  12540  elnnz1  12611  recnz  12662  uz3m2nn  12909  ledivge1le  13080  xrub  13329  1mod  13927  expubnd  14205  expnbnd  14259  expnlbnd  14260  hashgt23el  14451  resqrex  15291  sin02gt0  16238  oddge22np1  16397  dvdsnprmd  16738  prmlem1  17157  prmlem2  17170  lsmss2  19728  ovolicopnf  25644  voliunlem3  25672  volsup  25676  volivth  25727  itg2seq  25862  itg2monolem2  25871  reeff1olem  26567  sinq12gt0  26630  logdivlti  26743  logdivlt  26744  efexple  27403  gausslemma2dlem4  27491  axlowdimlem16  29216  axlowdimlem17  29217  axlowdim  29220  rusgr1vtx  29847  dmdbr2  32564  dfon2lem3  36146  dfon2lem7  36150  nn0prpwlem  36695  bj-resta  37598  tan2h  38123  mblfinlem4  38171  m1mod0mod1  47952  m1modmmod  47956  muldvdsfacgt  47978  muldvdsfacm1  47979  iccpartgt  48031  nprmdvdsfacm1lem4  48230  gbegt5  48381  gbowgt5  48382  sbgoldbalt  48401  sgoldbeven3prm  48403  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  evengpoap3  48419  nnsum4primesevenALTV  48421  regt1loggt0  49167  rege1logbrege0  49189  rege1logbzge0  49190