Theorem mpani 709

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mp2ani  711  frpoind  6338  ordelinel  6459  dif20el  8497  domunfican  9297  frind  9738  recgt1i  12195  recreclt  12197  ledivp1i  12223  nngt0  12350  nnrecgt0  12362  elnnnn0c  12632  elnnz1  12703  recnz  12755  uz3m2nn  13002  ledivge1le  13174  xrub  13423  1mod  14023  expubnd  14301  expnbnd  14356  expnlbnd  14357  hashgt23el  14549  resqrex  15397  sin02gt0  16340  oddge22np1  16499  dvdsnprmd  16845  prmlem1  17265  prmlem2  17278  lsmss2  19861  ovolicopnf  25825  voliunlem3  25853  volsup  25857  volivth  25908  itg2seq  26043  itg2monolem2  26052  reeff1olem  26755  sinq12gt0  26818  logdivlti  26930  logdivlt  26931  efexple  27590  gausslemma2dlem4  27678  axlowdimlem16  29517  axlowdimlem17  29518  axlowdim  29521  rusgr1vtx  30151  dmdbr2  32887  dfon2lem3  36517  dfon2lem7  36521  nn0prpwlem  37080  bj-resta  37985  tan2h  38503  mblfinlem4  38546  m1mod0mod1  48374  m1modmmod  48378  muldvdsfacgt  48400  muldvdsfacm1  48401  iccpartgt  48453  nprmdvdsfacm1lem4  48652  gbegt5  48803  gbowgt5  48804  sbgoldbalt  48823  sgoldbeven3prm  48825  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  evengpoap3  48841  nnsum4primesevenALTV  48843  regt1loggt0  49592  rege1logbrege0  49614  rege1logbzge0  49615