Theorem 3simpa 1148

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Assertion

Ref	Expression
3simpa	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

Proof of Theorem 3simpa

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2	1	3adant3 1132	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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:  3adantl3  1168  3adantr3  1171  disjtp2  4715  pr1eqbg  4856  preq12nebg  4862  otel3xp  5730  brcogw  5878  funtpg  6620  ftpg  7175  ovig  7580  el2xptp0  8062  fprresex  8336  wfrlem17OLD  8366  undifixp  8975  tz9.1c  9771  ackbij1lem16  10275  enqeq  10975  prlem934  11074  lt2halves  12503  nn0n0n1ge2  12596  ixxssixx  13402  ltdifltdiv  13875  hash2prd  14515  hashtpg  14525  pfxsuffeqwrdeq  14737  pfxccatpfx1  14775  pfxccatpfx2  14776  s3eq3seq  14979  sumtp  15786  dvdscmulr  16323  dvdsmulcr  16324  dvds2add  16328  dvds2sub  16329  dvdstr  16332  vdwlem12  17031  cshwsidrepswmod0  17133  cshwshashlem2  17135  initoeu2lem0  18059  estrreslem1  18182  estrreslem1OLD  18183  funcestrcsetclem9  18194  funcsetcestrclem9  18209  mhmismgmhm  18805  resmndismnd  18822  sgrp2nmndlem4  18942  dfgrp3e  19059  lmhmlem  21029  cnfldfunALT  21380  cnfldfunALTOLD  21393  psgndiflemA  21620  matsc  22457  scmatrhmcl  22535  mdetdiaglem  22605  decpmatid  22777  decpmatmullem  22778  mp2pm2mplem4  22816  chfacfisf  22861  chfacfisfcpmat  22862  cpmidgsumm2pm  22876  cpmidpmat  22880  cpmadumatpoly  22890  2ndcctbss  23464  dvfsumrlim  26073  dvfsumrlim2  26074  ulmval  26424  relogbmul  26821  conway  27845  axcontlem2  28981  uspgr1v1eop  29267  uhgrissubgr  29293  subgrprop3  29294  0uhgrsubgr  29297  wlkelwrd  29652  uhgrwkspth  29776  usgr2wlkspth  29780  2pthon3v  29964  uhgr3cyclex  30202  umgr3v3e3cycl  30204  numclwwlk1lem2foa  30374  numclwwlk5  30408  leopmul  32154  strlem3a  32272  0elsiga  34116  afsval  34687  bnj999  34973  subgrwlk  35138  cusgr3cyclex  35142  acycgrislfgr  35158  satfvsucsuc  35371  ex-sategoelel  35427  ex-sategoel  35428  cgr3permute3  36049  cgr3com  36055  colineardim1  36063  brofs2  36079  brifs2  36080  btwnconn1lem4  36092  btwnconn1lem5  36093  btwnconn1lem6  36094  midofsegid  36106  isbasisrelowllem1  37357  isbasisrelowllem2  37358  icoreclin  37359  ftc1anclem8  37708  sdclem2  37750  ismndo1  37881  refrelredund2  38638  lsmcv2  39031  lvolnleat  39586  paddasslem14  39836  4atexlemswapqr  40066  isltrn2N  40123  cdlemftr1  40570  cdlemg5  40608  iocinico  43229  omge1  43315  pwinfi2  43580  relexpxpnnidm  43721  pimxrneun  45504  sigaras  46875  sigarms  46876  difltmodne  47349  even3prm2  47711  fpprwpprb  47732  bgoldbtbndlem4  47800  bgoldbtbnd  47801  predgclnbgrel  47830  grimgrtri  47921  grlimgrtri  47968  funcringcsetcALTV2lem9  48219  funcringcsetclem9ALTV  48242  fprmappr  48266  gsumlsscl  48301  ldepspr  48395  lincresunit3lem3  48396  lincresunit3lem1  48401  lincresunit3  48403  reorelicc  48636  itsclc0yqsol  48690  itsclc0  48697