Theorem 3simpa 1164

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 1148	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3adantl3  1185  3adantr3  1188  disjtp2  4687  pr1eqbg  4826  preq12nebg  4832  otel3xp  5708  brcogw  5855  funtpg  6592  ftpg  7154  ovig  7557  el2xptp0  8032  fprresex  8306  undifixp  8931  tz9.1c  9698  ackbij1lem16  10216  enqeq  10918  prlem934  11017  lt2halves  12478  nn0n0n1ge2  12571  ixxssixx  13385  ltdifltdiv  13866  hash2prd  14511  hashtpg  14521  pfxsuffeqwrdeq  14734  pfxccatpfx1  14772  pfxccatpfx2  14773  s3eq3seq  14975  sumtp  15799  dvdscmulr  16341  dvdsmulcr  16342  dvds2add  16347  dvds2sub  16348  dvdstr  16351  vdwlem12  17051  cshwsidrepswmod0  17153  cshwshashlem2  17155  initoeu2lem0  18069  estrreslem1  18192  funcestrcsetclem9  18203  funcsetcestrclem9  18218  mhmismgmhm  18848  resmndismnd  18865  sgrp2nmndlem4  18989  dfgrp3e  19105  lmhmlem  21127  cnfldfunALT  21505  psgndiflemA  21719  matsc  22575  scmatrhmcl  22653  mdetdiaglem  22723  decpmatid  22895  decpmatmullem  22896  mp2pm2mplem4  22934  chfacfisf  22979  chfacfisfcpmat  22980  cpmidgsumm2pm  22994  cpmidpmat  22998  cpmadumatpoly  23008  2ndcctbss  23580  dvfsumrlim  26158  dvfsumrlim2  26159  ulmval  26508  relogbmul  26907  conway  27937  axcontlem2  29255  uspgr1v1eop  29539  uhgrissubgr  29565  subgrprop3  29566  0uhgrsubgr  29569  wlkelwrd  29922  uhgrwkspth  30044  usgr2wlkspth  30048  2pthon3v  30232  uhgr3cyclex  30473  umgr3v3e3cycl  30475  numclwwlk1lem2foa  30645  numclwwlk5  30679  leopmul  32426  strlem3a  32544  0elsiga  34448  afsval  35005  bnj999  35290  axprALT2  35444  tz9.1regs  35469  subgrwlk  35522  cusgr3cyclex  35526  acycgrislfgr  35542  satfvsucsuc  35755  ex-sategoelel  35811  ex-sategoel  35812  cgr3permute3  36437  cgr3com  36443  colineardim1  36451  brofs2  36467  brifs2  36468  btwnconn1lem4  36480  btwnconn1lem5  36481  btwnconn1lem6  36482  midofsegid  36494  ttcexg  36931  isbasisrelowllem1  37888  isbasisrelowllem2  37889  icoreclin  37890  ftc1anclem8  38238  sdclem2  38280  ismndo1  38411  refrelredund2  39258  lsmcv2  39692  lvolnleat  40246  paddasslem14  40496  4atexlemswapqr  40726  isltrn2N  40783  cdlemftr1  41230  cdlemg5  41268  iocinico  43830  omge1  43915  pwinfi2  44179  relexpxpnnidm  44320  pimxrneun  46093  sigaras  47460  sigarms  47461  difltmodne  47973  even3prm2  48372  fpprwpprb  48393  bgoldbtbndlem4  48461  bgoldbtbnd  48462  predgclnbgrel  48492  uhgrimprop  48545  grimgrtri  48602  grlimgrtri  48656  funcringcsetcALTV2lem9  48951  funcringcsetclem9ALTV  48974  fprmappr  49009  gsumlsscl  49044  ldepspr  49137  lincresunit3lem3  49138  lincresunit3lem1  49143  lincresunit3  49145  reorelicc  49374  itsclc0yqsol  49428  itsclc0  49435