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 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  6325  wrecseq2  8342  oeoalem  8632  mulrid  11256  addltmul  12499  eluzaddiOLD  12907  fz01en  13588  fznatpl1  13614  expubnd  14213  bernneq  14264  bernneq2  14265  faclbnd4lem1  14328  hashfun  14472  bpoly2  16089  bpoly3  16090  fsumcube  16092  efi4p  16169  efival  16184  cos2tsin  16211  cos01bnd  16218  cos01gt0  16223  dvds0  16305  odd2np1  16374  opoe  16396  divalglem0  16426  gcdid  16560  pythagtriplem4  16852  ressid  17289  fvpr0o  17605  fvpr1o  17606  zringcyg  21497  lecldbas  23242  blssioo  24830  tgioo  24831  rerest  24839  xrrest  24842  zdis  24851  reconnlem2  24862  metdscn2  24892  negcncf  24961  negcncfOLD  24962  iihalf2  24974  cncmet  25369  rrxmvallem  25451  rrxmval  25452  ovolunlem1a  25544  ismbf3d  25702  c1lip2  26051  pilem2  26510  pilem3  26511  sinperlem  26536  sincosq1sgn  26554  sincosq2sgn  26555  sinq12gt0  26563  cosq14gt0  26566  cosq14ge0  26567  coseq1  26581  sinord  26590  zetacvg  27072  1sgmprm  27257  ppiub  27262  chtublem  27269  chtub  27270  bcp1ctr  27337  bpos1lem  27340  bposlem2  27343  bposlem3  27344  bposlem4  27345  bposlem5  27346  bposlem6  27347  bposlem7  27348  bposlem9  27350  nnsge1  28360  cutpw2  28431  pw2bday  28432  pw2cut  28434  zs12bday  28438  axlowdim  28990  ipidsq  30738  ipasslem1  30859  ipasslem2  30860  ipasslem4  30862  ipasslem5  30863  ipasslem8  30865  ipasslem9  30866  ipasslem11  30868  pjoc1i  31459  h1de2bi  31582  h1de2ctlem  31583  spanunsni  31607  opsqrlem1  32168  opsqrlem6  32173  chrelati  32392  chrelat2i  32393  cvexchlem  32396  pnfinf  33172  1fldgenq  33303  rrhre  33983  erdszelem5  35179  wsuceq2  35797  taupilem1  37303  finxpreclem2  37372  sin2h  37596  cos2h  37597  tan2h  37598  poimirlem27  37633  poimirlem30  37636  broucube  37640  mblfinlem1  37643  heiborlem6  37802  lcmineqlem19  42028  2xp3dxp2ge1d  42222  onexomgt  43229  omabs2  43321  icccncfext  45842  dirkertrigeq  46056  zlmodzxzel  48199  dignn0flhalflem1  48464  2arymaptfo  48503  fv1prop  48548  fv2prop  48549  line2x  48603  onetansqsecsq  48991  cotsqcscsq  48992