Theorem mp3an13 1451

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 1449	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 687	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  predeq2  6303  wrecseq2  8310  oeoalem  8602  mulrid  11219  addltmul  12455  eluzaddiOLD  12861  fz01en  13536  fznatpl1  13562  expubnd  14149  bernneq  14199  bernneq2  14200  faclbnd4lem1  14260  hashfun  14404  bpoly2  16008  bpoly3  16009  fsumcube  16011  efi4p  16087  efival  16102  cos2tsin  16129  cos01bnd  16136  cos01gt0  16141  dvds0  16222  odd2np1  16291  opoe  16313  divalglem0  16343  gcdid  16475  pythagtriplem4  16759  ressid  17196  fvpr0o  17512  fvpr1o  17513  zringcyg  21328  lecldbas  23042  blssioo  24630  tgioo  24631  rerest  24639  xrrest  24642  zdis  24651  reconnlem2  24662  metdscn2  24692  negcncf  24761  negcncfOLD  24762  iihalf2  24774  cncmet  25169  rrxmvallem  25251  rrxmval  25252  ovolunlem1a  25344  ismbf3d  25502  c1lip2  25850  pilem2  26303  pilem3  26304  sinperlem  26329  sincosq1sgn  26347  sincosq2sgn  26348  sinq12gt0  26356  cosq14gt0  26359  cosq14ge0  26360  coseq1  26373  sinord  26382  zetacvg  26859  1sgmprm  27044  ppiub  27049  chtublem  27056  chtub  27057  bcp1ctr  27124  bpos1lem  27127  bposlem2  27130  bposlem3  27131  bposlem4  27132  bposlem5  27133  bposlem6  27134  bposlem7  27135  bposlem9  27137  axlowdim  28651  ipidsq  30395  ipasslem1  30516  ipasslem2  30517  ipasslem4  30519  ipasslem5  30520  ipasslem8  30522  ipasslem9  30523  ipasslem11  30525  pjoc1i  31116  h1de2bi  31239  h1de2ctlem  31240  spanunsni  31264  opsqrlem1  31825  opsqrlem6  31830  chrelati  32049  chrelat2i  32050  cvexchlem  32053  pnfinf  32764  1fldgenq  32847  rrhre  33464  erdszelem5  34649  wsuceq2  35257  taupilem1  36665  finxpreclem2  36734  sin2h  36941  cos2h  36942  tan2h  36943  poimirlem27  36978  poimirlem30  36981  broucube  36985  mblfinlem1  36988  heiborlem6  37147  lcmineqlem19  41378  2xp3dxp2ge1d  41488  onexomgt  42452  omabs2  42544  icccncfext  45061  dirkertrigeq  45275  zlmodzxzel  47193  dignn0flhalflem1  47462  2arymaptfo  47501  fv1prop  47546  fv2prop  47547  line2x  47601  onetansqsecsq  47967  cotsqcscsq  47968