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  6252  wrecseq2  8249  oeoalem  8514  mulrid  11113  addltmul  12360  eluzaddiOLD  12767  fz01en  13455  fznatpl1  13481  expubnd  14085  bernneq  14136  bernneq2  14137  faclbnd4lem1  14200  hashfun  14344  bpoly2  15964  bpoly3  15965  fsumcube  15967  efi4p  16046  efival  16061  cos2tsin  16088  cos01bnd  16095  cos01gt0  16100  dvds0  16182  odd2np1  16252  opoe  16274  divalglem0  16304  gcdid  16438  pythagtriplem4  16731  ressid  17155  fvpr0o  17463  fvpr1o  17464  zringcyg  21376  lecldbas  23104  blssioo  24681  tgioo  24682  rerest  24690  xrrest  24694  zdis  24703  reconnlem2  24714  metdscn2  24744  negcncf  24813  negcncfOLD  24814  iihalf2  24826  cncmet  25220  rrxmvallem  25302  rrxmval  25303  ovolunlem1a  25395  ismbf3d  25553  c1lip2  25901  pilem2  26360  pilem3  26361  sinperlem  26387  sincosq1sgn  26405  sincosq2sgn  26406  sinq12gt0  26414  cosq14gt0  26417  cosq14ge0  26418  coseq1  26432  sinord  26441  zetacvg  26923  1sgmprm  27108  ppiub  27113  chtublem  27120  chtub  27121  bcp1ctr  27188  bpos1lem  27191  bposlem2  27194  bposlem3  27195  bposlem4  27196  bposlem5  27197  bposlem6  27198  bposlem7  27199  bposlem9  27201  nnsge1  28242  pw2gt0divsd  28339  pw2ge0divsd  28340  pw2sltdivmuld  28344  pw2sltmuldiv2d  28345  pw2cut  28351  zs12bday  28365  axlowdim  28910  ipidsq  30658  ipasslem1  30779  ipasslem2  30780  ipasslem4  30782  ipasslem5  30783  ipasslem8  30785  ipasslem9  30786  ipasslem11  30788  pjoc1i  31379  h1de2bi  31502  h1de2ctlem  31503  spanunsni  31527  opsqrlem1  32088  opsqrlem6  32093  chrelati  32312  chrelat2i  32313  cvexchlem  32316  pnfinf  33134  1fldgenq  33270  rrhre  34004  erdszelem5  35188  wsuceq2  35810  taupilem1  37315  finxpreclem2  37384  sin2h  37610  cos2h  37611  tan2h  37612  poimirlem27  37647  poimirlem30  37650  broucube  37654  mblfinlem1  37657  heiborlem6  37816  lcmineqlem19  42040  onexomgt  43234  omabs2  43325  icccncfext  45888  dirkertrigeq  46102  pgnbgreunbgrlem4  48123  zlmodzxzel  48359  dignn0flhalflem1  48620  2arymaptfo  48659  fv1prop  48704  fv2prop  48705  line2x  48759  onetansqsecsq  49766  cotsqcscsq  49767