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  6280  wrecseq2  8298  oeoalem  8563  mulrid  11179  addltmul  12425  eluzaddiOLD  12832  fz01en  13520  fznatpl1  13546  expubnd  14150  bernneq  14201  bernneq2  14202  faclbnd4lem1  14265  hashfun  14409  bpoly2  16030  bpoly3  16031  fsumcube  16033  efi4p  16112  efival  16127  cos2tsin  16154  cos01bnd  16161  cos01gt0  16166  dvds0  16248  odd2np1  16318  opoe  16340  divalglem0  16370  gcdid  16504  pythagtriplem4  16797  ressid  17221  fvpr0o  17529  fvpr1o  17530  zringcyg  21386  lecldbas  23113  blssioo  24690  tgioo  24691  rerest  24699  xrrest  24703  zdis  24712  reconnlem2  24723  metdscn2  24753  negcncf  24822  negcncfOLD  24823  iihalf2  24835  cncmet  25229  rrxmvallem  25311  rrxmval  25312  ovolunlem1a  25404  ismbf3d  25562  c1lip2  25910  pilem2  26369  pilem3  26370  sinperlem  26396  sincosq1sgn  26414  sincosq2sgn  26415  sinq12gt0  26423  cosq14gt0  26426  cosq14ge0  26427  coseq1  26441  sinord  26450  zetacvg  26932  1sgmprm  27117  ppiub  27122  chtublem  27129  chtub  27130  bcp1ctr  27197  bpos1lem  27200  bposlem2  27203  bposlem3  27204  bposlem4  27205  bposlem5  27206  bposlem6  27207  bposlem7  27208  bposlem9  27210  nnsge1  28242  pw2gt0divsd  28335  pw2ge0divsd  28336  pw2cut  28342  zs12bday  28350  axlowdim  28895  ipidsq  30646  ipasslem1  30767  ipasslem2  30768  ipasslem4  30770  ipasslem5  30771  ipasslem8  30773  ipasslem9  30774  ipasslem11  30776  pjoc1i  31367  h1de2bi  31490  h1de2ctlem  31491  spanunsni  31515  opsqrlem1  32076  opsqrlem6  32081  chrelati  32300  chrelat2i  32301  cvexchlem  32304  pnfinf  33144  1fldgenq  33279  rrhre  34018  erdszelem5  35189  wsuceq2  35811  taupilem1  37316  finxpreclem2  37385  sin2h  37611  cos2h  37612  tan2h  37613  poimirlem27  37648  poimirlem30  37651  broucube  37655  mblfinlem1  37658  heiborlem6  37817  lcmineqlem19  42042  onexomgt  43237  omabs2  43328  icccncfext  45892  dirkertrigeq  46106  pgnbgreunbgrlem4  48113  zlmodzxzel  48347  dignn0flhalflem1  48608  2arymaptfo  48647  fv1prop  48692  fv2prop  48693  line2x  48747  onetansqsecsq  49754  cotsqcscsq  49755