Theorem 3simpa 1147

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 1131	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  1167  3adantr3  1170  disjtp2  4721  pr1eqbg  4862  preq12nebg  4868  otel3xp  5735  brcogw  5882  funtpg  6623  ftpg  7176  ovig  7579  el2xptp0  8060  fprresex  8334  wfrlem17OLD  8364  undifixp  8973  tz9.1c  9768  ackbij1lem16  10272  enqeq  10972  prlem934  11071  lt2halves  12499  nn0n0n1ge2  12592  ixxssixx  13398  ltdifltdiv  13871  hash2prd  14511  hashtpg  14521  pfxsuffeqwrdeq  14733  pfxccatpfx1  14771  pfxccatpfx2  14772  s3eq3seq  14975  sumtp  15782  dvdscmulr  16319  dvdsmulcr  16320  dvds2add  16324  dvds2sub  16325  dvdstr  16328  vdwlem12  17026  cshwsidrepswmod0  17129  cshwshashlem2  17131  initoeu2lem0  18067  estrreslem1  18192  estrreslem1OLD  18193  funcestrcsetclem9  18204  funcsetcestrclem9  18219  mhmismgmhm  18817  resmndismnd  18834  sgrp2nmndlem4  18954  dfgrp3e  19071  lmhmlem  21046  cnfldfunALT  21397  cnfldfunALTOLD  21410  psgndiflemA  21637  matsc  22472  scmatrhmcl  22550  mdetdiaglem  22620  decpmatid  22792  decpmatmullem  22793  mp2pm2mplem4  22831  chfacfisf  22876  chfacfisfcpmat  22877  cpmidgsumm2pm  22891  cpmidpmat  22895  cpmadumatpoly  22905  2ndcctbss  23479  dvfsumrlim  26087  dvfsumrlim2  26088  ulmval  26438  relogbmul  26835  conway  27859  axcontlem2  28995  uspgr1v1eop  29281  uhgrissubgr  29307  subgrprop3  29308  0uhgrsubgr  29311  wlkelwrd  29666  uhgrwkspth  29788  usgr2wlkspth  29792  2pthon3v  29973  uhgr3cyclex  30211  umgr3v3e3cycl  30213  numclwwlk1lem2foa  30383  numclwwlk5  30417  leopmul  32163  strlem3a  32281  0elsiga  34095  afsval  34665  bnj999  34951  subgrwlk  35117  cusgr3cyclex  35121  acycgrislfgr  35137  satfvsucsuc  35350  ex-sategoelel  35406  ex-sategoel  35407  cgr3permute3  36029  cgr3com  36035  colineardim1  36043  brofs2  36059  brifs2  36060  btwnconn1lem4  36072  btwnconn1lem5  36073  btwnconn1lem6  36074  midofsegid  36086  isbasisrelowllem1  37338  isbasisrelowllem2  37339  icoreclin  37340  ftc1anclem8  37687  sdclem2  37729  ismndo1  37860  refrelredund2  38618  lsmcv2  39011  lvolnleat  39566  paddasslem14  39816  4atexlemswapqr  40046  isltrn2N  40103  cdlemftr1  40550  cdlemg5  40588  iocinico  43201  omge1  43287  pwinfi2  43552  relexpxpnnidm  43693  pimxrneun  45439  sigaras  46811  sigarms  46812  difltmodne  47282  even3prm2  47644  fpprwpprb  47665  bgoldbtbndlem4  47733  bgoldbtbnd  47734  predgclnbgrel  47763  grimgrtri  47852  grlimgrtri  47899  funcringcsetcALTV2lem9  48142  funcringcsetclem9ALTV  48165  fprmappr  48190  gsumlsscl  48225  ldepspr  48319  lincresunit3lem3  48320  lincresunit3lem1  48325  lincresunit3  48327  reorelicc  48560  itsclc0yqsol  48614  itsclc0  48621