Theorem 3simpa 1148

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

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

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 1088

This theorem is referenced by:  3adantl3  1169  3adantr3  1172  disjtp2  4666  pr1eqbg  4806  preq12nebg  4812  otel3xp  5660  brcogw  5807  funtpg  6536  ftpg  7089  ovig  7492  el2xptp0  7968  fprresex  8240  undifixp  8858  tz9.1c  9620  ackbij1lem16  10125  enqeq  10825  prlem934  10924  lt2halves  12356  nn0n0n1ge2  12449  ixxssixx  13259  ltdifltdiv  13738  hash2prd  14382  hashtpg  14392  pfxsuffeqwrdeq  14605  pfxccatpfx1  14643  pfxccatpfx2  14644  s3eq3seq  14846  sumtp  15656  dvdscmulr  16195  dvdsmulcr  16196  dvds2add  16201  dvds2sub  16202  dvdstr  16205  vdwlem12  16904  cshwsidrepswmod0  17006  cshwshashlem2  17008  initoeu2lem0  17920  estrreslem1  18043  funcestrcsetclem9  18054  funcsetcestrclem9  18069  mhmismgmhm  18699  resmndismnd  18716  sgrp2nmndlem4  18836  dfgrp3e  18953  lmhmlem  20963  cnfldfunALT  21306  cnfldfunALTOLD  21319  psgndiflemA  21538  matsc  22365  scmatrhmcl  22443  mdetdiaglem  22513  decpmatid  22685  decpmatmullem  22686  mp2pm2mplem4  22724  chfacfisf  22769  chfacfisfcpmat  22770  cpmidgsumm2pm  22784  cpmidpmat  22788  cpmadumatpoly  22798  2ndcctbss  23370  dvfsumrlim  25965  dvfsumrlim2  25966  ulmval  26316  relogbmul  26714  conway  27740  axcontlem2  28943  uspgr1v1eop  29227  uhgrissubgr  29253  subgrprop3  29254  0uhgrsubgr  29257  wlkelwrd  29611  uhgrwkspth  29733  usgr2wlkspth  29737  2pthon3v  29921  uhgr3cyclex  30162  umgr3v3e3cycl  30164  numclwwlk1lem2foa  30334  numclwwlk5  30368  leopmul  32114  strlem3a  32232  0elsiga  34127  afsval  34684  bnj999  34970  tz9.1regs  35130  subgrwlk  35176  cusgr3cyclex  35180  acycgrislfgr  35196  satfvsucsuc  35409  ex-sategoelel  35465  ex-sategoel  35466  cgr3permute3  36089  cgr3com  36095  colineardim1  36103  brofs2  36119  brifs2  36120  btwnconn1lem4  36132  btwnconn1lem5  36133  btwnconn1lem6  36134  midofsegid  36146  isbasisrelowllem1  37397  isbasisrelowllem2  37398  icoreclin  37399  ftc1anclem8  37748  sdclem2  37790  ismndo1  37921  refrelredund2  38681  lsmcv2  39076  lvolnleat  39630  paddasslem14  39880  4atexlemswapqr  40110  isltrn2N  40167  cdlemftr1  40614  cdlemg5  40652  iocinico  43253  omge1  43338  pwinfi2  43603  relexpxpnnidm  43744  pimxrneun  45534  sigaras  46901  sigarms  46902  difltmodne  47381  even3prm2  47758  fpprwpprb  47779  bgoldbtbndlem4  47847  bgoldbtbnd  47848  predgclnbgrel  47878  uhgrimprop  47931  grimgrtri  47988  grlimgrtri  48042  funcringcsetcALTV2lem9  48337  funcringcsetclem9ALTV  48360  fprmappr  48384  gsumlsscl  48419  ldepspr  48513  lincresunit3lem3  48514  lincresunit3lem1  48519  lincresunit3  48521  reorelicc  48750  itsclc0yqsol  48804  itsclc0  48811