Theorem mp3an13 1450

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  predeq2  6202  wrecseq2  8119  oeoalem  8403  mulid1  10957  addltmul  12192  eluzaddi  12593  fz01en  13266  fznatpl1  13292  expubnd  13876  bernneq  13925  bernneq2  13926  faclbnd4lem1  13988  hashfun  14133  bpoly2  15748  bpoly3  15749  fsumcube  15751  efi4p  15827  efival  15842  cos2tsin  15869  cos01bnd  15876  cos01gt0  15881  dvds0  15962  odd2np1  16031  opoe  16053  divalglem0  16083  gcdid  16215  pythagtriplem4  16501  ressid  16935  fvpr0o  17251  fvpr1o  17252  zringcyg  20672  lecldbas  22351  blssioo  23939  tgioo  23940  rerest  23948  xrrest  23951  zdis  23960  reconnlem2  23971  metdscn2  24001  negcncf  24066  iihalf2  24077  cncmet  24467  rrxmvallem  24549  rrxmval  24550  ovolunlem1a  24641  ismbf3d  24799  c1lip2  25143  pilem2  25592  pilem3  25593  sinperlem  25618  sincosq1sgn  25636  sincosq2sgn  25637  sinq12gt0  25645  cosq14gt0  25648  cosq14ge0  25649  coseq1  25662  sinord  25671  zetacvg  26145  1sgmprm  26328  ppiub  26333  chtublem  26340  chtub  26341  bcp1ctr  26408  bpos1lem  26411  bposlem2  26414  bposlem3  26415  bposlem4  26416  bposlem5  26417  bposlem6  26418  bposlem7  26419  bposlem9  26421  axlowdim  27310  ipidsq  29051  ipasslem1  29172  ipasslem2  29173  ipasslem4  29175  ipasslem5  29176  ipasslem8  29178  ipasslem9  29179  ipasslem11  29181  pjoc1i  29772  h1de2bi  29895  h1de2ctlem  29896  spanunsni  29920  opsqrlem1  30481  opsqrlem6  30486  chrelati  30705  chrelat2i  30706  cvexchlem  30709  pnfinf  31416  rrhre  31950  erdszelem5  33136  wsuceq2  33789  taupilem1  35471  finxpreclem2  35540  sin2h  35746  cos2h  35747  tan2h  35748  poimirlem27  35783  poimirlem30  35786  broucube  35790  mblfinlem1  35793  heiborlem6  35953  lcmineqlem19  40035  2xp3dxp2ge1d  40142  icccncfext  43382  dirkertrigeq  43596  zlmodzxzel  45643  dignn0flhalflem1  45913  2arymaptfo  45952  fv1prop  45997  fv2prop  45998  line2x  46052  onetansqsecsq  46415  cotsqcscsq  46416