Theorem mp3an13 1480

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

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

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 401  df-3an 1104

This theorem is used by:  predeq2  6305  wrecseq2  8311  oeoalem  8580  mulrid  11212  addltmul  12486  fz01en  13587  fznatpl1  13613  expubnd  14221  bernneq  14272  bernneq2  14273  faclbnd4lem1  14336  hashfun  14481  bpoly2  16117  bpoly3  16118  fsumcube  16120  efi4p  16199  efival  16214  cos2tsin  16241  cos01bnd  16248  cos01gt0  16253  dvds0  16335  odd2np1  16405  opoe  16427  divalglem0  16457  gcdid  16591  pythagtriplem4  16885  ressid  17310  fvpr0o  17619  fvpr1o  17620  zringcyg  21630  lecldbas  23387  blssioo  24963  tgioo  24964  rerest  24972  xrrest  24976  zdis  24985  reconnlem2  24996  metdscn2  25026  negcncf  25092  iihalf2  25103  cncmet  25492  rrxmvallem  25574  rrxmval  25575  ovolunlem1a  25666  ismbf3d  25824  c1lip2  26168  pilem2  26626  pilem3  26627  sinperlem  26656  sincosq1sgn  26674  sincosq2sgn  26675  sinq12gt0  26683  cosq14gt0  26686  cosq14ge0  26687  coseq1  26701  sinord  26710  zetacvg  27190  1sgmprm  27374  ppiub  27379  chtublem  27386  chtub  27387  bcp1ctr  27454  bpos1lem  27457  bposlem2  27460  bposlem3  27461  bposlem4  27462  bposlem5  27463  bposlem6  27464  bposlem7  27465  bposlem9  27467  nnsge1  28547  pw2gt0divsd  28649  pw2ge0divsd  28650  pw2ltdivmulsd  28654  pw2ltmuldivs2d  28655  pw2ltdivmuls2d  28661  pw2cut  28664  bdayfinbndlem1  28671  axlowdim  29322  ipidsq  31073  ipasslem1  31194  ipasslem2  31195  ipasslem4  31197  ipasslem5  31198  ipasslem8  31200  ipasslem9  31201  ipasslem11  31203  pjoc1i  31794  h1de2bi  31917  h1de2ctlem  31918  spanunsni  31942  opsqrlem1  32503  opsqrlem6  32508  chrelati  32727  chrelat2i  32728  cvexchlem  32731  pnfinf  33512  1fldgenq  33652  rrhre  34420  erdszelem5  35695  wsuceq2  36314  taupilem1  37993  finxpreclem2  38064  sin2h  38289  cos2h  38290  tan2h  38291  poimirlem27  38326  poimirlem30  38329  broucube  38333  mblfinlem1  38336  heiborlem6  38495  lcmineqlem19  42842  onexomgt  43996  omabs2  44087  icccncfext  46629  dirkertrigeq  46843  pgnbgreunbgrlem4  48912  zlmodzxzel  49163  dignn0flhalflem1  49423  2arymaptfo  49462  fv1prop  49507  fv2prop  49508  line2x  49562  onetansqsecsq  50567  cotsqcscsq  50568