Theorem mpani 695

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  mp2ani  697  frpoind  6344  wfiOLD  6353  ordelinel  6466  dif20el  8505  domunfican  9320  frind  9745  mulgt1  12073  recgt1i  12111  recreclt  12113  ledivp1i  12139  nngt0  12243  nnrecgt0  12255  elnnnn0c  12517  elnnz1  12588  recnz  12637  uz3m2nn  12875  ledivge1le  13045  xrub  13291  1mod  13868  expubnd  14142  expnbnd  14195  expnlbnd  14196  hashgt23el  14384  resqrex  15197  sin02gt0  16135  oddge22np1  16292  dvdsnprmd  16627  prmlem1  17041  prmlem2  17053  lsmss2  19535  ovolicopnf  25041  voliunlem3  25069  volsup  25073  volivth  25124  itg2seq  25260  itg2monolem2  25269  reeff1olem  25958  sinq12gt0  26017  logdivlti  26128  logdivlt  26129  efexple  26784  gausslemma2dlem4  26872  axlowdimlem16  28215  axlowdimlem17  28216  axlowdim  28219  rusgr1vtx  28845  dmdbr2  31556  dfon2lem3  34757  dfon2lem7  34761  nn0prpwlem  35207  bj-resta  35977  tan2h  36480  mblfinlem4  36528  m1mod0mod1  46037  iccpartgt  46095  gbegt5  46429  gbowgt5  46430  sbgoldbalt  46449  sgoldbeven3prm  46451  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  evengpoap3  46467  nnsum4primesevenALTV  46469  m1modmmod  47207  difmodm1lt  47208  regt1loggt0  47222  rege1logbrege0  47244  rege1logbzge0  47245