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 1087

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 1089

This theorem is referenced by:  predeq2  6324  wrecseq2  8344  oeoalem  8634  mulrid  11259  addltmul  12502  eluzaddiOLD  12910  fz01en  13592  fznatpl1  13618  expubnd  14217  bernneq  14268  bernneq2  14269  faclbnd4lem1  14332  hashfun  14476  bpoly2  16093  bpoly3  16094  fsumcube  16096  efi4p  16173  efival  16188  cos2tsin  16215  cos01bnd  16222  cos01gt0  16227  dvds0  16309  odd2np1  16378  opoe  16400  divalglem0  16430  gcdid  16564  pythagtriplem4  16857  ressid  17290  fvpr0o  17604  fvpr1o  17605  zringcyg  21480  lecldbas  23227  blssioo  24816  tgioo  24817  rerest  24825  xrrest  24829  zdis  24838  reconnlem2  24849  metdscn2  24879  negcncf  24948  negcncfOLD  24949  iihalf2  24961  cncmet  25356  rrxmvallem  25438  rrxmval  25439  ovolunlem1a  25531  ismbf3d  25689  c1lip2  26037  pilem2  26496  pilem3  26497  sinperlem  26522  sincosq1sgn  26540  sincosq2sgn  26541  sinq12gt0  26549  cosq14gt0  26552  cosq14ge0  26553  coseq1  26567  sinord  26576  zetacvg  27058  1sgmprm  27243  ppiub  27248  chtublem  27255  chtub  27256  bcp1ctr  27323  bpos1lem  27326  bposlem2  27329  bposlem3  27330  bposlem4  27331  bposlem5  27332  bposlem6  27333  bposlem7  27334  bposlem9  27336  nnsge1  28346  cutpw2  28417  pw2bday  28418  pw2cut  28420  zs12bday  28424  axlowdim  28976  ipidsq  30729  ipasslem1  30850  ipasslem2  30851  ipasslem4  30853  ipasslem5  30854  ipasslem8  30856  ipasslem9  30857  ipasslem11  30859  pjoc1i  31450  h1de2bi  31573  h1de2ctlem  31574  spanunsni  31598  opsqrlem1  32159  opsqrlem6  32164  chrelati  32383  chrelat2i  32384  cvexchlem  32387  pnfinf  33190  1fldgenq  33324  rrhre  34022  erdszelem5  35200  wsuceq2  35817  taupilem1  37322  finxpreclem2  37391  sin2h  37617  cos2h  37618  tan2h  37619  poimirlem27  37654  poimirlem30  37657  broucube  37661  mblfinlem1  37664  heiborlem6  37823  lcmineqlem19  42048  2xp3dxp2ge1d  42242  onexomgt  43253  omabs2  43345  icccncfext  45902  dirkertrigeq  46116  zlmodzxzel  48271  dignn0flhalflem1  48536  2arymaptfo  48575  fv1prop  48620  fv2prop  48621  line2x  48675  onetansqsecsq  49280  cotsqcscsq  49281