Theorem mpani 712

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  mp2ani  714  wfi  5713  ordelinel  5825  ordelinelOLD  5826  dif20el  7585  domunfican  8233  mulgt1  10882  recgt1i  10920  recreclt  10922  ledivp1i  10949  nngt0  11049  nnrecgt0  11058  elnnnn0c  11338  elnnz1  11403  recnz  11452  uz3m2nn  11731  ledivge1le  11901  xrub  12142  1mod  12702  expubnd  12921  expnbnd  12993  expnlbnd  12994  resqrex  13991  sin02gt0  14922  oddge22np1  15073  dvdsnprmd  15403  prmlem1  15814  prmlem2  15827  lsmss2  18081  ovolicopnf  23292  voliunlem3  23320  volsup  23324  volivth  23375  itg2seq  23509  itg2monolem2  23518  reeff1olem  24200  sinq12gt0  24259  logdivlti  24366  logdivlt  24367  efexple  25006  gausslemma2dlem4  25094  axlowdimlem16  25837  axlowdimlem17  25838  axlowdim  25841  rusgr1vtx  26484  dmdbr2  29162  dfon2lem3  31690  dfon2lem7  31694  frind  31740  nn0prpwlem  32317  bj-resta  33049  tan2h  33401  mblfinlem4  33449  m1mod0mod1  41339  iccpartgt  41363  pfx2  41412  gbegt5  41649  gbowgt5  41650  sbgoldbalt  41669  sgoldbeven3prm  41671  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  evengpoap3  41687  nnsum4primesevenALTV  41689  m1modmmod  42316  difmodm1lt  42317  regt1loggt0  42330  rege1logbrege0  42352  rege1logbzge0  42353