Theorem mp3an13 1454

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  predeq2  6265  wrecseq2  8272  oeoalem  8537  mulrid  11150  addltmul  12396  eluzaddiOLD  12803  fz01en  13491  fznatpl1  13517  expubnd  14121  bernneq  14172  bernneq2  14173  faclbnd4lem1  14236  hashfun  14380  bpoly2  16000  bpoly3  16001  fsumcube  16003  efi4p  16082  efival  16097  cos2tsin  16124  cos01bnd  16131  cos01gt0  16136  dvds0  16218  odd2np1  16288  opoe  16310  divalglem0  16340  gcdid  16474  pythagtriplem4  16767  ressid  17191  fvpr0o  17499  fvpr1o  17500  zringcyg  21412  lecldbas  23140  blssioo  24717  tgioo  24718  rerest  24726  xrrest  24730  zdis  24739  reconnlem2  24750  metdscn2  24780  negcncf  24849  negcncfOLD  24850  iihalf2  24862  cncmet  25256  rrxmvallem  25338  rrxmval  25339  ovolunlem1a  25431  ismbf3d  25589  c1lip2  25937  pilem2  26396  pilem3  26397  sinperlem  26423  sincosq1sgn  26441  sincosq2sgn  26442  sinq12gt0  26450  cosq14gt0  26453  cosq14ge0  26454  coseq1  26468  sinord  26477  zetacvg  26959  1sgmprm  27144  ppiub  27149  chtublem  27156  chtub  27157  bcp1ctr  27224  bpos1lem  27227  bposlem2  27230  bposlem3  27231  bposlem4  27232  bposlem5  27233  bposlem6  27234  bposlem7  27235  bposlem9  27237  nnsge1  28276  pw2gt0divsd  28373  pw2ge0divsd  28374  pw2sltdivmuld  28378  pw2sltmuldiv2d  28379  pw2cut  28384  zs12bday  28397  axlowdim  28942  ipidsq  30690  ipasslem1  30811  ipasslem2  30812  ipasslem4  30814  ipasslem5  30815  ipasslem8  30817  ipasslem9  30818  ipasslem11  30820  pjoc1i  31411  h1de2bi  31534  h1de2ctlem  31535  spanunsni  31559  opsqrlem1  32120  opsqrlem6  32125  chrelati  32344  chrelat2i  32345  cvexchlem  32348  pnfinf  33153  1fldgenq  33289  rrhre  34005  erdszelem5  35176  wsuceq2  35798  taupilem1  37303  finxpreclem2  37372  sin2h  37598  cos2h  37599  tan2h  37600  poimirlem27  37635  poimirlem30  37638  broucube  37642  mblfinlem1  37645  heiborlem6  37804  lcmineqlem19  42029  onexomgt  43224  omabs2  43315  icccncfext  45879  dirkertrigeq  46093  pgnbgreunbgrlem4  48103  zlmodzxzel  48337  dignn0flhalflem1  48598  2arymaptfo  48637  fv1prop  48682  fv2prop  48683  line2x  48737  onetansqsecsq  49744  cotsqcscsq  49745