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 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  6277  wrecseq2  8295  oeoalem  8560  mulrid  11172  addltmul  12418  eluzaddiOLD  12825  fz01en  13513  fznatpl1  13539  expubnd  14143  bernneq  14194  bernneq2  14195  faclbnd4lem1  14258  hashfun  14402  bpoly2  16023  bpoly3  16024  fsumcube  16026  efi4p  16105  efival  16120  cos2tsin  16147  cos01bnd  16154  cos01gt0  16159  dvds0  16241  odd2np1  16311  opoe  16333  divalglem0  16363  gcdid  16497  pythagtriplem4  16790  ressid  17214  fvpr0o  17522  fvpr1o  17523  zringcyg  21379  lecldbas  23106  blssioo  24683  tgioo  24684  rerest  24692  xrrest  24696  zdis  24705  reconnlem2  24716  metdscn2  24746  negcncf  24815  negcncfOLD  24816  iihalf2  24828  cncmet  25222  rrxmvallem  25304  rrxmval  25305  ovolunlem1a  25397  ismbf3d  25555  c1lip2  25903  pilem2  26362  pilem3  26363  sinperlem  26389  sincosq1sgn  26407  sincosq2sgn  26408  sinq12gt0  26416  cosq14gt0  26419  cosq14ge0  26420  coseq1  26434  sinord  26443  zetacvg  26925  1sgmprm  27110  ppiub  27115  chtublem  27122  chtub  27123  bcp1ctr  27190  bpos1lem  27193  bposlem2  27196  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem7  27201  bposlem9  27203  nnsge1  28235  pw2gt0divsd  28328  pw2ge0divsd  28329  pw2cut  28335  zs12bday  28343  axlowdim  28888  ipidsq  30639  ipasslem1  30760  ipasslem2  30761  ipasslem4  30763  ipasslem5  30764  ipasslem8  30766  ipasslem9  30767  ipasslem11  30769  pjoc1i  31360  h1de2bi  31483  h1de2ctlem  31484  spanunsni  31508  opsqrlem1  32069  opsqrlem6  32074  chrelati  32293  chrelat2i  32294  cvexchlem  32297  pnfinf  33137  1fldgenq  33272  rrhre  34011  erdszelem5  35182  wsuceq2  35804  taupilem1  37309  finxpreclem2  37378  sin2h  37604  cos2h  37605  tan2h  37606  poimirlem27  37641  poimirlem30  37644  broucube  37648  mblfinlem1  37651  heiborlem6  37810  lcmineqlem19  42035  onexomgt  43230  omabs2  43321  icccncfext  45885  dirkertrigeq  46099  pgnbgreunbgrlem4  48109  zlmodzxzel  48343  dignn0flhalflem1  48604  2arymaptfo  48643  fv1prop  48688  fv2prop  48689  line2x  48743  onetansqsecsq  49750  cotsqcscsq  49751