Theorem 3simpa 1149

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3adantl3  1170  3adantr3  1173  disjtp2  4675  pr1eqbg  4815  preq12nebg  4821  otel3xp  5678  brcogw  5825  funtpg  6555  ftpg  7111  ovig  7514  el2xptp0  7990  fprresex  8262  undifixp  8884  tz9.1c  9651  ackbij1lem16  10156  enqeq  10857  prlem934  10956  lt2halves  12388  nn0n0n1ge2  12481  ixxssixx  13287  ltdifltdiv  13766  hash2prd  14410  hashtpg  14420  pfxsuffeqwrdeq  14633  pfxccatpfx1  14671  pfxccatpfx2  14672  s3eq3seq  14874  sumtp  15684  dvdscmulr  16223  dvdsmulcr  16224  dvds2add  16229  dvds2sub  16230  dvdstr  16233  vdwlem12  16932  cshwsidrepswmod0  17034  cshwshashlem2  17036  initoeu2lem0  17949  estrreslem1  18072  funcestrcsetclem9  18083  funcsetcestrclem9  18098  mhmismgmhm  18728  resmndismnd  18745  sgrp2nmndlem4  18865  dfgrp3e  18982  lmhmlem  20993  cnfldfunALT  21336  cnfldfunALTOLD  21349  psgndiflemA  21568  matsc  22406  scmatrhmcl  22484  mdetdiaglem  22554  decpmatid  22726  decpmatmullem  22727  mp2pm2mplem4  22765  chfacfisf  22810  chfacfisfcpmat  22811  cpmidgsumm2pm  22825  cpmidpmat  22829  cpmadumatpoly  22839  2ndcctbss  23411  dvfsumrlim  26006  dvfsumrlim2  26007  ulmval  26357  relogbmul  26755  conway  27787  axcontlem2  29050  uspgr1v1eop  29334  uhgrissubgr  29360  subgrprop3  29361  0uhgrsubgr  29364  wlkelwrd  29718  uhgrwkspth  29840  usgr2wlkspth  29844  2pthon3v  30028  uhgr3cyclex  30269  umgr3v3e3cycl  30271  numclwwlk1lem2foa  30441  numclwwlk5  30475  leopmul  32222  strlem3a  32340  0elsiga  34292  afsval  34849  bnj999  35134  axprALT2  35287  tz9.1regs  35312  subgrwlk  35348  cusgr3cyclex  35352  acycgrislfgr  35368  satfvsucsuc  35581  ex-sategoelel  35637  ex-sategoel  35638  cgr3permute3  36263  cgr3com  36269  colineardim1  36277  brofs2  36293  brifs2  36294  btwnconn1lem4  36306  btwnconn1lem5  36307  btwnconn1lem6  36308  midofsegid  36320  isbasisrelowllem1  37610  isbasisrelowllem2  37611  icoreclin  37612  ftc1anclem8  37951  sdclem2  37993  ismndo1  38124  refrelredund2  38971  lsmcv2  39405  lvolnleat  39959  paddasslem14  40209  4atexlemswapqr  40439  isltrn2N  40496  cdlemftr1  40943  cdlemg5  40981  iocinico  43569  omge1  43654  pwinfi2  43918  relexpxpnnidm  44059  pimxrneun  45846  sigaras  47213  sigarms  47214  difltmodne  47702  even3prm2  48079  fpprwpprb  48100  bgoldbtbndlem4  48168  bgoldbtbnd  48169  predgclnbgrel  48199  uhgrimprop  48252  grimgrtri  48309  grlimgrtri  48363  funcringcsetcALTV2lem9  48658  funcringcsetclem9ALTV  48681  fprmappr  48705  gsumlsscl  48740  ldepspr  48833  lincresunit3lem3  48834  lincresunit3lem1  48839  lincresunit3  48841  reorelicc  49070  itsclc0yqsol  49124  itsclc0  49131