Theorem mp3an13 1455

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 1453	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 691	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  6261  wrecseq2  8258  oeoalem  8524  mulrid  11132  addltmul  12379  fz01en  13470  fznatpl1  13496  expubnd  14103  bernneq  14154  bernneq2  14155  faclbnd4lem1  14218  hashfun  14362  bpoly2  15982  bpoly3  15983  fsumcube  15985  efi4p  16064  efival  16079  cos2tsin  16106  cos01bnd  16113  cos01gt0  16118  dvds0  16200  odd2np1  16270  opoe  16292  divalglem0  16322  gcdid  16456  pythagtriplem4  16749  ressid  17173  fvpr0o  17482  fvpr1o  17483  zringcyg  21426  lecldbas  23165  blssioo  24741  tgioo  24742  rerest  24750  xrrest  24754  zdis  24763  reconnlem2  24774  metdscn2  24804  negcncf  24873  negcncfOLD  24874  iihalf2  24886  cncmet  25280  rrxmvallem  25362  rrxmval  25363  ovolunlem1a  25455  ismbf3d  25613  c1lip2  25961  pilem2  26420  pilem3  26421  sinperlem  26447  sincosq1sgn  26465  sincosq2sgn  26466  sinq12gt0  26474  cosq14gt0  26477  cosq14ge0  26478  coseq1  26492  sinord  26501  zetacvg  26983  1sgmprm  27168  ppiub  27173  chtublem  27180  chtub  27181  bcp1ctr  27248  bpos1lem  27251  bposlem2  27254  bposlem3  27255  bposlem4  27256  bposlem5  27257  bposlem6  27258  bposlem7  27259  bposlem9  27261  nnsge1  28321  pw2gt0divsd  28422  pw2ge0divsd  28423  pw2sltdivmuld  28427  pw2sltmuldiv2d  28428  pw2sltdivmul2d  28434  pw2cut  28437  bdayfinbndlem1  28444  axlowdim  29015  ipidsq  30766  ipasslem1  30887  ipasslem2  30888  ipasslem4  30890  ipasslem5  30891  ipasslem8  30893  ipasslem9  30894  ipasslem11  30896  pjoc1i  31487  h1de2bi  31610  h1de2ctlem  31611  spanunsni  31635  opsqrlem1  32196  opsqrlem6  32201  chrelati  32420  chrelat2i  32421  cvexchlem  32424  pnfinf  33244  1fldgenq  33383  rrhre  34157  erdszelem5  35368  wsuceq2  35987  taupilem1  37495  finxpreclem2  37564  sin2h  37780  cos2h  37781  tan2h  37782  poimirlem27  37817  poimirlem30  37820  broucube  37824  mblfinlem1  37827  heiborlem6  37986  lcmineqlem19  42336  onexomgt  43520  omabs2  43611  icccncfext  46168  dirkertrigeq  46382  pgnbgreunbgrlem4  48402  zlmodzxzel  48638  dignn0flhalflem1  48898  2arymaptfo  48937  fv1prop  48982  fv2prop  48983  line2x  49037  onetansqsecsq  50043  cotsqcscsq  50044