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  4677  pr1eqbg  4817  preq12nebg  4823  otel3xp  5701  brcogw  5848  funtpg  6588  ftpg  7153  ovig  7559  el2xptp0  8033  fprresex  8309  undifixp  8941  tz9.1c  9709  ackbij1lem16  10236  enqeq  10943  prlem934  11042  lt2halves  12503  nn0n0n1ge2  12596  ixxssixx  13412  ltdifltdiv  13895  hash2prd  14540  hashtpg  14550  pfxsuffeqwrdeq  14767  pfxccatpfx1  14805  pfxccatpfx2  14806  s3eq3seq  15010  sumtp  15835  dvdscmulr  16374  dvdsmulcr  16375  dvds2add  16380  dvds2sub  16381  dvdstr  16384  vdwlem12  17084  cshwsidrepswmod0  17186  cshwshashlem2  17188  initoeu2lem0  18102  estrreslem1  18225  funcestrcsetclem9  18236  funcsetcestrclem9  18251  mhmismgmhm  18899  resmndismnd  18916  sgrp2nmndlem4  19040  dfgrp3e  19163  lmhmlem  21213  cnfldfunALT  21600  psgndiflemA  21814  matsc  22672  scmatrhmcl  22750  mdetdiaglem  22820  decpmatid  22995  decpmatmullem  22996  mp2pm2mplem4  23034  chfacfisf  23079  chfacfisfcpmat  23080  cpmidgsumm2pm  23094  cpmidpmat  23098  cpmadumatpoly  23108  2ndcctbss  23681  dvfsumrlim  26258  dvfsumrlim2  26259  ulmval  26616  relogbmul  27014  conway  28044  axcontlem2  29422  uspgr1v1eop  29709  uhgrissubgr  29735  subgrprop3  29736  0uhgrsubgr  29739  wlkelwrd  30092  subgrwlk  30148  uhgrwkspth  30220  usgr2wlkspth  30224  2pthon3v  30411  uhgr3cyclex  30662  umgr3v3e3cycl  30664  numclwwlk1lem2foa  30834  numclwwlk5  30868  leopmul  32615  strlem3a  32733  0elsiga  34624  afsval  35182  bnj999  35467  axprALT2  35617  tz9.1regs  35660  cusgr3cyclex  35725  acycgrislfgr  35731  satfvsucsuc  35944  ex-sategoelel  36000  ex-sategoel  36001  cgr3permute3  36627  cgr3com  36633  colineardim1  36641  brofs2  36657  brifs2  36658  btwnconn1lem4  36670  btwnconn1lem5  36671  btwnconn1lem6  36672  midofsegid  36684  ttcexg  37151  isbasisrelowllem1  38109  isbasisrelowllem2  38110  icoreclin  38111  ftc1anclem8  38449  sdclem2  38492  ismndo1  38623  refrelredund2  39468  lsmcv2  39902  lvolnleat  40456  paddasslem14  40706  4atexlemswapqr  40936  isltrn2N  40993  cdlemftr1  41440  cdlemg5  41478  iocinico  44053  omge1  44138  pwinfi2  44402  relexpxpnnidm  44543  pimxrneun  46316  sigaras  47683  sigarms  47684  difltmodne  48236  even3prm2  48635  fpprwpprb  48656  bgoldbtbndlem4  48724  bgoldbtbnd  48725  predgclnbgrel  48755  uhgrimprop  48808  grimgrtri  48865  grlimgrtri  48919  funcringcsetcALTV2lem9  49213  funcringcsetclem9ALTV  49236  fprmappr  49275  gsumlsscl  49310  ldepspr  49403  lincresunit3lem3  49404  lincresunit3lem1  49409  lincresunit3  49411  reorelicc  49640  itsclc0yqsol  49694  itsclc0  49701