Theorem mp3an13 1481

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an13.1	⊢ 𝜑
mp3an13.2	⊢ 𝜒
mp3an13.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an13	⊢ (𝜓 → 𝜃)

Proof of Theorem mp3an13

Step	Hyp	Ref	Expression
1		mp3an13.1	. 2 ⊢ 𝜑
2		mp3an13.2	. . 3 ⊢ 𝜒
3		mp3an13.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1479	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 703	1 ⊢ (𝜓 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

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  df-3an 1105

This theorem is used by:  predeq2  6307  wrecseq2  8334  oeoalem  8605  mulrid  11306  addltmul  12582  fz01en  13686  fznatpl1  13712  expubnd  14321  bernneq  14373  bernneq2  14374  faclbnd4lem1  14437  hashfun  14582  bpoly2  16223  bpoly3  16224  fsumcube  16226  efi4p  16305  efival  16320  cos2tsin  16347  cos01bnd  16354  cos01gt0  16359  dvds0  16441  odd2np1  16511  opoe  16533  divalglem0  16563  gcdid  16699  pythagtriplem4  16997  ressid  17422  fvpr0o  17731  fvpr1o  17732  zringcyg  21775  lecldbas  23537  blssioo  25114  tgioo  25115  rerest  25123  xrrest  25127  zdis  25136  reconnlem2  25147  metdscn2  25177  negcncf  25243  iihalf2  25254  cncmet  25643  rrxmvallem  25725  rrxmval  25726  ovolunlem1a  25817  ismbf3d  25975  c1lip2  26318  pilem2  26779  pilem3  26780  sinperlem  26809  sincosq1sgn  26827  sincosq2sgn  26828  sinq12gt0  26836  cosq14gt0  26839  cosq14ge0  26840  coseq1  26853  sinord  26862  zetacvg  27342  1sgmprm  27526  ppiub  27531  chtublem  27538  chtub  27539  bcp1ctr  27606  bpos1lem  27609  bposlem2  27612  bposlem3  27613  bposlem4  27614  bposlem5  27615  bposlem6  27616  bposlem7  27617  bposlem9  27619  nnsge1  28729  pw2gt0divsd  28831  pw2ge0divsd  28832  pw2ltdivmulsd  28836  pw2ltmuldivs2d  28837  pw2ltdivmuls2d  28843  pw2cut  28846  bdayfinbndlem1  28853  axlowdim  29539  ipidsq  31312  ipasslem1  31433  ipasslem2  31434  ipasslem4  31436  ipasslem5  31437  ipasslem8  31439  ipasslem9  31440  ipasslem11  31442  pjoc1i  32033  h1de2bi  32156  h1de2ctlem  32157  spanunsni  32181  opsqrlem1  32742  opsqrlem6  32747  chrelati  32966  chrelat2i  32967  cvexchlem  32970  pnfinf  33744  1fldgenq  33884  rrhre  34653  erdszelem5  35960  wsuceq2  36578  taupilem1  38243  finxpreclem2  38314  sin2h  38534  cos2h  38535  tan2h  38536  poimirlem27  38566  poimirlem30  38569  broucube  38573  mblfinlem1  38576  heiborlem6  38751  lcmineqlem19  43098  onexomgt  44243  omabs2  44334  icccncfext  46897  dirkertrigeq  47111  pgnbgreunbgrlem4  49217  zlmodzxzel  49467  dignn0flhalflem1  49727  2arymaptfo  49766  fv1prop  49811  fv2prop  49812  line2x  49866  onetansqsecsq  50854  cotsqcscsq  50855