Theorem mp3an13 1415

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

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  predeq2  5683  wrecseq2  7411  oeoalem  7676  mulid1  10037  addltmul  11268  eluzaddi  11714  fz01en  12369  fznatpl1  12395  expubnd  12921  bernneq  12990  bernneq2  12991  faclbnd4lem1  13080  hashfun  13224  bpoly2  14788  bpoly3  14789  fsumcube  14791  efi4p  14867  efival  14882  cos2tsin  14909  cos01bnd  14916  cos01gt0  14921  dvds0  14997  odd2np1  15065  opoe  15087  divalglem0  15116  gcdid  15248  pythagtriplem4  15524  ressid  15935  zringcyg  19839  lecldbas  21023  blssioo  22598  tgioo  22599  rerest  22607  xrrest  22610  zdis  22619  reconnlem2  22630  metdscn2  22660  negcncf  22721  iihalf2  22732  cncmet  23119  rrxmvallem  23187  rrxmval  23188  ovolunlem1a  23264  ismbf3d  23421  c1lip2  23761  pilem2  24206  pilem3  24207  sinperlem  24232  sincosq1sgn  24250  sincosq2sgn  24251  sinq12gt0  24259  cosq14gt0  24262  cosq14ge0  24263  coseq1  24274  sinord  24280  zetacvg  24741  1sgmprm  24924  ppiub  24929  chtublem  24936  chtub  24937  bcp1ctr  25004  bpos1lem  25007  bposlem2  25010  bposlem3  25011  bposlem4  25012  bposlem5  25013  bposlem6  25014  bposlem7  25015  bposlem9  25017  axlowdim  25841  ipidsq  27565  ipasslem1  27686  ipasslem2  27687  ipasslem4  27689  ipasslem5  27690  ipasslem8  27692  ipasslem9  27693  ipasslem11  27695  pjoc1i  28290  h1de2bi  28413  h1de2ctlem  28414  spanunsni  28438  opsqrlem1  28999  opsqrlem6  29004  chrelati  29223  chrelat2i  29224  cvexchlem  29227  pnfinf  29737  rrhre  30065  erdszelem5  31177  wsuceq2  31762  taupilem1  33167  finxpreclem2  33227  sin2h  33399  cos2h  33400  tan2h  33401  poimirlem27  33436  poimirlem30  33439  broucube  33443  mblfinlem1  33446  heiborlem6  33615  icccncfext  40100  dirkertrigeq  40318  zlmodzxzel  42133  dignn0flhalflem1  42409  onetansqsecsq  42502  cotsqcscsq  42503