Theorem mp3an13 1452

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 1450	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 689	1 ⊢ (𝜓 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  predeq2  6335  wrecseq2  8360  oeoalem  8652  mulrid  11288  addltmul  12529  eluzaddiOLD  12935  fz01en  13612  fznatpl1  13638  expubnd  14227  bernneq  14278  bernneq2  14279  faclbnd4lem1  14342  hashfun  14486  bpoly2  16105  bpoly3  16106  fsumcube  16108  efi4p  16185  efival  16200  cos2tsin  16227  cos01bnd  16234  cos01gt0  16239  dvds0  16320  odd2np1  16389  opoe  16411  divalglem0  16441  gcdid  16573  pythagtriplem4  16866  ressid  17303  fvpr0o  17619  fvpr1o  17620  zringcyg  21503  lecldbas  23248  blssioo  24836  tgioo  24837  rerest  24845  xrrest  24848  zdis  24857  reconnlem2  24868  metdscn2  24898  negcncf  24967  negcncfOLD  24968  iihalf2  24980  cncmet  25375  rrxmvallem  25457  rrxmval  25458  ovolunlem1a  25550  ismbf3d  25708  c1lip2  26057  pilem2  26514  pilem3  26515  sinperlem  26540  sincosq1sgn  26558  sincosq2sgn  26559  sinq12gt0  26567  cosq14gt0  26570  cosq14ge0  26571  coseq1  26585  sinord  26594  zetacvg  27076  1sgmprm  27261  ppiub  27266  chtublem  27273  chtub  27274  bcp1ctr  27341  bpos1lem  27344  bposlem2  27347  bposlem3  27348  bposlem4  27349  bposlem5  27350  bposlem6  27351  bposlem7  27352  bposlem9  27354  nnsge1  28364  cutpw2  28435  pw2bday  28436  pw2cut  28438  zs12bday  28442  axlowdim  28994  ipidsq  30742  ipasslem1  30863  ipasslem2  30864  ipasslem4  30866  ipasslem5  30867  ipasslem8  30869  ipasslem9  30870  ipasslem11  30872  pjoc1i  31463  h1de2bi  31586  h1de2ctlem  31587  spanunsni  31611  opsqrlem1  32172  opsqrlem6  32177  chrelati  32396  chrelat2i  32397  cvexchlem  32400  pnfinf  33163  1fldgenq  33289  rrhre  33967  erdszelem5  35163  wsuceq2  35780  taupilem1  37287  finxpreclem2  37356  sin2h  37570  cos2h  37571  tan2h  37572  poimirlem27  37607  poimirlem30  37610  broucube  37614  mblfinlem1  37617  heiborlem6  37776  lcmineqlem19  42004  2xp3dxp2ge1d  42198  onexomgt  43202  omabs2  43294  icccncfext  45808  dirkertrigeq  46022  zlmodzxzel  48080  dignn0flhalflem1  48349  2arymaptfo  48388  fv1prop  48433  fv2prop  48434  line2x  48488  onetansqsecsq  48853  cotsqcscsq  48854