Theorem mp3an13 1475

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

Syntax hints:   → wi 4   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  predeq2  6293  wrecseq2  8299  oeoalem  8568  mulrid  11181  addltmul  12459  fz01en  13559  fznatpl1  13585  expubnd  14193  bernneq  14244  bernneq2  14245  faclbnd4lem1  14308  hashfun  14452  bpoly2  16089  bpoly3  16090  fsumcube  16092  efi4p  16171  efival  16186  cos2tsin  16213  cos01bnd  16220  cos01gt0  16225  dvds0  16307  odd2np1  16377  opoe  16399  divalglem0  16429  gcdid  16563  pythagtriplem4  16857  ressid  17282  fvpr0o  17591  fvpr1o  17592  zringcyg  21523  lecldbas  23281  blssioo  24857  tgioo  24858  rerest  24866  xrrest  24870  zdis  24879  reconnlem2  24890  metdscn2  24920  negcncf  24986  iihalf2  24997  cncmet  25386  rrxmvallem  25468  rrxmval  25469  ovolunlem1a  25560  ismbf3d  25718  c1lip2  26062  pilem2  26517  pilem3  26518  sinperlem  26547  sincosq1sgn  26565  sincosq2sgn  26566  sinq12gt0  26574  cosq14gt0  26577  cosq14ge0  26578  coseq1  26592  sinord  26601  zetacvg  27081  1sgmprm  27265  ppiub  27270  chtublem  27277  chtub  27278  bcp1ctr  27345  bpos1lem  27348  bposlem2  27351  bposlem3  27352  bposlem4  27353  bposlem5  27354  bposlem6  27355  bposlem7  27356  bposlem9  27358  nnsge1  28438  pw2gt0divsd  28540  pw2ge0divsd  28541  pw2ltdivmulsd  28545  pw2ltmuldivs2d  28546  pw2ltdivmuls2d  28552  pw2cut  28555  bdayfinbndlem1  28562  axlowdim  29164  ipidsq  30915  ipasslem1  31036  ipasslem2  31037  ipasslem4  31039  ipasslem5  31040  ipasslem8  31042  ipasslem9  31043  ipasslem11  31045  pjoc1i  31636  h1de2bi  31759  h1de2ctlem  31760  spanunsni  31784  opsqrlem1  32345  opsqrlem6  32350  chrelati  32569  chrelat2i  32570  cvexchlem  32573  pnfinf  33365  1fldgenq  33511  rrhre  34320  erdszelem5  35550  wsuceq2  36169  taupilem1  37818  finxpreclem2  37889  sin2h  38114  cos2h  38115  tan2h  38116  poimirlem27  38151  poimirlem30  38154  broucube  38158  mblfinlem1  38161  heiborlem6  38320  lcmineqlem19  42669  onexomgt  43823  omabs2  43914  icccncfext  46466  dirkertrigeq  46680  pgnbgreunbgrlem4  48746  zlmodzxzel  48982  dignn0flhalflem1  49242  2arymaptfo  49281  fv1prop  49326  fv2prop  49327  line2x  49381  onetansqsecsq  50387  cotsqcscsq  50388