Theorem 3simpa 1161

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3adantl3  1182  3adantr3  1185  disjtp2  4675  pr1eqbg  4815  preq12nebg  4821  otel3xp  5693  brcogw  5840  funtpg  6576  ftpg  7139  ovig  7542  el2xptp0  8017  fprresex  8291  undifixp  8916  tz9.1c  9685  ackbij1lem16  10190  enqeq  10892  prlem934  10991  lt2halves  12456  nn0n0n1ge2  12549  ixxssixx  13363  ltdifltdiv  13844  hash2prd  14488  hashtpg  14498  pfxsuffeqwrdeq  14711  pfxccatpfx1  14749  pfxccatpfx2  14750  s3eq3seq  14952  sumtp  15776  dvdscmulr  16318  dvdsmulcr  16319  dvds2add  16324  dvds2sub  16325  dvdstr  16328  vdwlem12  17028  cshwsidrepswmod0  17130  cshwshashlem2  17132  initoeu2lem0  18046  estrreslem1  18169  funcestrcsetclem9  18180  funcsetcestrclem9  18195  mhmismgmhm  18825  resmndismnd  18842  sgrp2nmndlem4  18965  dfgrp3e  19082  lmhmlem  21093  cnfldfunALT  21436  psgndiflemA  21650  matsc  22507  scmatrhmcl  22585  mdetdiaglem  22655  decpmatid  22827  decpmatmullem  22828  mp2pm2mplem4  22866  chfacfisf  22911  chfacfisfcpmat  22912  cpmidgsumm2pm  22926  cpmidpmat  22930  cpmadumatpoly  22940  2ndcctbss  23512  dvfsumrlim  26090  dvfsumrlim2  26091  ulmval  26440  relogbmul  26839  conway  27869  axcontlem2  29163  uspgr1v1eop  29447  uhgrissubgr  29473  subgrprop3  29474  0uhgrsubgr  29477  wlkelwrd  29830  uhgrwkspth  29952  usgr2wlkspth  29956  2pthon3v  30140  uhgr3cyclex  30381  umgr3v3e3cycl  30383  numclwwlk1lem2foa  30553  numclwwlk5  30587  leopmul  32334  strlem3a  32452  0elsiga  34408  afsval  34965  bnj999  35250  axprALT2  35402  tz9.1regs  35427  subgrwlk  35479  cusgr3cyclex  35483  acycgrislfgr  35499  satfvsucsuc  35712  ex-sategoelel  35768  ex-sategoel  35769  cgr3permute3  36394  cgr3com  36400  colineardim1  36408  brofs2  36424  brifs2  36425  btwnconn1lem4  36437  btwnconn1lem5  36438  btwnconn1lem6  36439  midofsegid  36451  ttcexg  36889  isbasisrelowllem1  37846  isbasisrelowllem2  37847  icoreclin  37848  ftc1anclem8  38196  sdclem2  38238  ismndo1  38369  refrelredund2  39216  lsmcv2  39650  lvolnleat  40204  paddasslem14  40454  4atexlemswapqr  40684  isltrn2N  40741  cdlemftr1  41188  cdlemg5  41226  iocinico  43786  omge1  43871  pwinfi2  44135  relexpxpnnidm  44276  pimxrneun  46059  sigaras  47426  sigarms  47427  difltmodne  47939  even3prm2  48338  fpprwpprb  48359  bgoldbtbndlem4  48427  bgoldbtbnd  48428  predgclnbgrel  48458  uhgrimprop  48511  grimgrtri  48568  grlimgrtri  48622  funcringcsetcALTV2lem9  48917  funcringcsetclem9ALTV  48940  fprmappr  48964  gsumlsscl  48999  ldepspr  49092  lincresunit3lem3  49093  lincresunit3lem1  49098  lincresunit3  49100  reorelicc  49329  itsclc0yqsol  49383  itsclc0  49390