Theorem 3simpa 1166

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 23	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2	1	3adant3 1150	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adantl3  1187  3adantr3  1190  disjtp2  4676  pr1eqbg  4816  preq12nebg  4822  otel3xp  5696  brcogw  5845  funtpg  6595  ftpg  7160  ovig  7566  el2xptp0  8047  fprresex  8329  undifixp  8963  tz9.1c  9732  ackbij1lem16  10313  enqeq  11020  prlem934  11119  lt2halves  12582  nn0n0n1ge2  12675  ixxssixx  13491  ltdifltdiv  13975  hash2prd  14621  hashtpg  14631  pfxsuffeqwrdeq  14848  pfxccatpfx1  14886  pfxccatpfx2  14887  s3eq3seq  15091  sumtp  15916  dvdscmulr  16455  dvdsmulcr  16456  dvds2add  16461  dvds2sub  16462  dvdstr  16465  vdwlem12  17171  cshwsidrepswmod0  17273  cshwshashlem2  17275  initoeu2lem0  18189  estrreslem1  18312  funcestrcsetclem9  18323  funcsetcestrclem9  18338  mhmismgmhm  18987  resmndismnd  19004  sgrp2nmndlem4  19128  dfgrp3e  19251  lmhmlem  21305  cnfldfunALT  21694  psgndiflemA  21908  matsc  22766  scmatrhmcl  22844  mdetdiaglem  22914  decpmatid  23089  decpmatmullem  23090  mp2pm2mplem4  23128  chfacfisf  23173  chfacfisfcpmat  23174  cpmidgsumm2pm  23188  cpmidpmat  23192  cpmadumatpoly  23202  2ndcctbss  23775  dvfsumrlim  26352  dvfsumrlim2  26353  ulmval  26708  relogbmul  27106  conway  28166  axcontlem2  29544  uspgr1v1eop  29831  uhgrissubgr  29857  subgrprop3  29858  0uhgrsubgr  29861  wlkelwrd  30214  subgrwlk  30270  uhgrwkspth  30342  usgr2wlkspth  30346  2pthon3v  30533  uhgr3cyclex  30784  umgr3v3e3cycl  30786  numclwwlk1lem2foa  30956  numclwwlk5  30990  leopmul  32737  strlem3a  32855  0elsiga  34789  afsval  35346  bnj999  35631  axprALT2  35777  tz9.1regs  35845  cusgr3cyclex  35954  acycgrislfgr  35960  satfvsucsuc  36173  ex-sategoelel  36229  ex-sategoel  36230  cgr3permute3  36855  cgr3com  36861  colineardim1  36869  brofs2  36885  brifs2  36886  btwnconn1lem4  36898  btwnconn1lem5  36899  btwnconn1lem6  36900  midofsegid  36912  ttcexg  37363  isbasisrelowllem1  38322  isbasisrelowllem2  38323  icoreclin  38324  ftc1anclem8  38662  sdclem2  38720  ismndo1  38851  refrelredund2  39696  lsmcv2  40130  lvolnleat  40684  paddasslem14  40934  4atexlemswapqr  41164  isltrn2N  41221  cdlemftr1  41668  cdlemg5  41706  iocinico  44258  omge1  44343  pwinfi2  44607  relexpxpnnidm  44747  pimxrneun  46542  sigaras  47909  sigarms  47910  difltmodne  48462  even3prm2  48861  fpprwpprb  48882  bgoldbtbndlem4  48950  bgoldbtbnd  48951  predgclnbgrel  48981  uhgrimprop  49034  grimgrtri  49091  grlimgrtri  49145  funcringcsetcALTV2lem9  49439  funcringcsetclem9ALTV  49462  fprmappr  49501  gsumlsscl  49536  ldepspr  49629  lincresunit3lem3  49630  lincresunit3lem1  49635  lincresunit3  49637  reorelicc  49866  itsclc0yqsol  49920  itsclc0  49927