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  4684  pr1eqbg  4824  preq12nebg  4830  otel3xp  5709  brcogw  5856  funtpg  6595  ftpg  7159  ovig  7565  el2xptp0  8039  fprresex  8313  undifixp  8938  tz9.1c  9706  ackbij1lem16  10233  enqeq  10934  prlem934  11033  lt2halves  12494  nn0n0n1ge2  12587  ixxssixx  13402  ltdifltdiv  13885  hash2prd  14530  hashtpg  14540  pfxsuffeqwrdeq  14757  pfxccatpfx1  14795  pfxccatpfx2  14796  s3eq3seq  15000  sumtp  15823  dvdscmulr  16364  dvdsmulcr  16365  dvds2add  16370  dvds2sub  16371  dvdstr  16374  vdwlem12  17074  cshwsidrepswmod0  17176  cshwshashlem2  17178  initoeu2lem0  18092  estrreslem1  18215  funcestrcsetclem9  18226  funcsetcestrclem9  18241  mhmismgmhm  18886  resmndismnd  18903  sgrp2nmndlem4  19027  dfgrp3e  19150  lmhmlem  21200  cnfldfunALT  21587  psgndiflemA  21801  matsc  22657  scmatrhmcl  22735  mdetdiaglem  22805  decpmatid  22977  decpmatmullem  22978  mp2pm2mplem4  23016  chfacfisf  23061  chfacfisfcpmat  23062  cpmidgsumm2pm  23076  cpmidpmat  23080  cpmadumatpoly  23090  2ndcctbss  23663  dvfsumrlim  26241  dvfsumrlim2  26242  ulmval  26594  relogbmul  26993  conway  28023  axcontlem2  29370  uspgr1v1eop  29657  uhgrissubgr  29683  subgrprop3  29684  0uhgrsubgr  29687  wlkelwrd  30040  subgrwlk  30096  uhgrwkspth  30168  usgr2wlkspth  30172  2pthon3v  30359  uhgr3cyclex  30604  umgr3v3e3cycl  30606  numclwwlk1lem2foa  30776  numclwwlk5  30810  leopmul  32557  strlem3a  32675  0elsiga  34568  afsval  35126  bnj999  35411  axprALT2  35561  tz9.1regs  35604  cusgr3cyclex  35669  acycgrislfgr  35681  satfvsucsuc  35894  ex-sategoelel  35950  ex-sategoel  35951  cgr3permute3  36576  cgr3com  36582  colineardim1  36590  brofs2  36606  brifs2  36607  btwnconn1lem4  36619  btwnconn1lem5  36620  btwnconn1lem6  36621  midofsegid  36633  ttcexg  37100  isbasisrelowllem1  38058  isbasisrelowllem2  38059  icoreclin  38060  ftc1anclem8  38408  sdclem2  38451  ismndo1  38582  refrelredund2  39427  lsmcv2  39861  lvolnleat  40415  paddasslem14  40665  4atexlemswapqr  40895  isltrn2N  40952  cdlemftr1  41399  cdlemg5  41437  iocinico  43997  omge1  44082  pwinfi2  44346  relexpxpnnidm  44487  pimxrneun  46260  sigaras  47627  sigarms  47628  difltmodne  48143  even3prm2  48542  fpprwpprb  48563  bgoldbtbndlem4  48631  bgoldbtbnd  48632  predgclnbgrel  48662  uhgrimprop  48715  grimgrtri  48772  grlimgrtri  48826  funcringcsetcALTV2lem9  49120  funcringcsetclem9ALTV  49143  fprmappr  49182  gsumlsscl  49217  ldepspr  49310  lincresunit3lem3  49311  lincresunit3lem1  49316  lincresunit3  49318  reorelicc  49547  itsclc0yqsol  49601  itsclc0  49608