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  1169  3adantr3  1172  disjtp2  4671  pr1eqbg  4811  preq12nebg  4817  otel3xp  5668  brcogw  5815  funtpg  6545  ftpg  7099  ovig  7502  el2xptp0  7978  fprresex  8250  undifixp  8870  tz9.1c  9637  ackbij1lem16  10142  enqeq  10843  prlem934  10942  lt2halves  12374  nn0n0n1ge2  12467  ixxssixx  13273  ltdifltdiv  13752  hash2prd  14396  hashtpg  14406  pfxsuffeqwrdeq  14619  pfxccatpfx1  14657  pfxccatpfx2  14658  s3eq3seq  14860  sumtp  15670  dvdscmulr  16209  dvdsmulcr  16210  dvds2add  16215  dvds2sub  16216  dvdstr  16219  vdwlem12  16918  cshwsidrepswmod0  17020  cshwshashlem2  17022  initoeu2lem0  17935  estrreslem1  18058  funcestrcsetclem9  18069  funcsetcestrclem9  18084  mhmismgmhm  18714  resmndismnd  18731  sgrp2nmndlem4  18851  dfgrp3e  18968  lmhmlem  20979  cnfldfunALT  21322  cnfldfunALTOLD  21335  psgndiflemA  21554  matsc  22392  scmatrhmcl  22470  mdetdiaglem  22540  decpmatid  22712  decpmatmullem  22713  mp2pm2mplem4  22751  chfacfisf  22796  chfacfisfcpmat  22797  cpmidgsumm2pm  22811  cpmidpmat  22815  cpmadumatpoly  22825  2ndcctbss  23397  dvfsumrlim  25992  dvfsumrlim2  25993  ulmval  26343  relogbmul  26741  conway  27767  axcontlem2  28987  uspgr1v1eop  29271  uhgrissubgr  29297  subgrprop3  29298  0uhgrsubgr  29301  wlkelwrd  29655  uhgrwkspth  29777  usgr2wlkspth  29781  2pthon3v  29965  uhgr3cyclex  30206  umgr3v3e3cycl  30208  numclwwlk1lem2foa  30378  numclwwlk5  30412  leopmul  32158  strlem3a  32276  0elsiga  34220  afsval  34777  bnj999  35063  tz9.1regs  35239  subgrwlk  35275  cusgr3cyclex  35279  acycgrislfgr  35295  satfvsucsuc  35508  ex-sategoelel  35564  ex-sategoel  35565  cgr3permute3  36190  cgr3com  36196  colineardim1  36204  brofs2  36220  brifs2  36221  btwnconn1lem4  36233  btwnconn1lem5  36234  btwnconn1lem6  36235  midofsegid  36247  isbasisrelowllem1  37499  isbasisrelowllem2  37500  icoreclin  37501  ftc1anclem8  37840  sdclem2  37882  ismndo1  38013  refrelredund2  38832  lsmcv2  39228  lvolnleat  39782  paddasslem14  40032  4atexlemswapqr  40262  isltrn2N  40319  cdlemftr1  40766  cdlemg5  40804  iocinico  43396  omge1  43481  pwinfi2  43745  relexpxpnnidm  43886  pimxrneun  45674  sigaras  47041  sigarms  47042  difltmodne  47530  even3prm2  47907  fpprwpprb  47928  bgoldbtbndlem4  47996  bgoldbtbnd  47997  predgclnbgrel  48027  uhgrimprop  48080  grimgrtri  48137  grlimgrtri  48191  funcringcsetcALTV2lem9  48486  funcringcsetclem9ALTV  48509  fprmappr  48533  gsumlsscl  48568  ldepspr  48661  lincresunit3lem3  48662  lincresunit3lem1  48667  lincresunit3  48669  reorelicc  48898  itsclc0yqsol  48952  itsclc0  48959