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  4676  pr1eqbg  4817  preq12nebg  4823  otel3xp  5677  brcogw  5822  funtpg  6555  ftpg  7110  ovig  7515  el2xptp0  7994  fprresex  8266  undifixp  8884  tz9.1c  9659  ackbij1lem16  10163  enqeq  10863  prlem934  10962  lt2halves  12393  nn0n0n1ge2  12486  ixxssixx  13296  ltdifltdiv  13772  hash2prd  14416  hashtpg  14426  pfxsuffeqwrdeq  14639  pfxccatpfx1  14677  pfxccatpfx2  14678  s3eq3seq  14881  sumtp  15691  dvdscmulr  16230  dvdsmulcr  16231  dvds2add  16236  dvds2sub  16237  dvdstr  16240  vdwlem12  16939  cshwsidrepswmod0  17041  cshwshashlem2  17043  initoeu2lem0  17951  estrreslem1  18074  funcestrcsetclem9  18085  funcsetcestrclem9  18100  mhmismgmhm  18694  resmndismnd  18711  sgrp2nmndlem4  18831  dfgrp3e  18948  lmhmlem  20912  cnfldfunALT  21255  cnfldfunALTOLD  21268  psgndiflemA  21486  matsc  22313  scmatrhmcl  22391  mdetdiaglem  22461  decpmatid  22633  decpmatmullem  22634  mp2pm2mplem4  22672  chfacfisf  22717  chfacfisfcpmat  22718  cpmidgsumm2pm  22732  cpmidpmat  22736  cpmadumatpoly  22746  2ndcctbss  23318  dvfsumrlim  25914  dvfsumrlim2  25915  ulmval  26265  relogbmul  26663  conway  27687  axcontlem2  28868  uspgr1v1eop  29152  uhgrissubgr  29178  subgrprop3  29179  0uhgrsubgr  29182  wlkelwrd  29536  uhgrwkspth  29658  usgr2wlkspth  29662  2pthon3v  29846  uhgr3cyclex  30084  umgr3v3e3cycl  30086  numclwwlk1lem2foa  30256  numclwwlk5  30290  leopmul  32036  strlem3a  32154  0elsiga  34077  afsval  34635  bnj999  34921  subgrwlk  35092  cusgr3cyclex  35096  acycgrislfgr  35112  satfvsucsuc  35325  ex-sategoelel  35381  ex-sategoel  35382  cgr3permute3  36008  cgr3com  36014  colineardim1  36022  brofs2  36038  brifs2  36039  btwnconn1lem4  36051  btwnconn1lem5  36052  btwnconn1lem6  36053  midofsegid  36065  isbasisrelowllem1  37316  isbasisrelowllem2  37317  icoreclin  37318  ftc1anclem8  37667  sdclem2  37709  ismndo1  37840  refrelredund2  38600  lsmcv2  38995  lvolnleat  39550  paddasslem14  39800  4atexlemswapqr  40030  isltrn2N  40087  cdlemftr1  40534  cdlemg5  40572  iocinico  43174  omge1  43259  pwinfi2  43524  relexpxpnnidm  43665  pimxrneun  45457  sigaras  46826  sigarms  46827  difltmodne  47316  even3prm2  47693  fpprwpprb  47714  bgoldbtbndlem4  47782  bgoldbtbnd  47783  predgclnbgrel  47812  uhgrimprop  47865  grimgrtri  47921  grlimgrtri  47968  funcringcsetcALTV2lem9  48259  funcringcsetclem9ALTV  48282  fprmappr  48306  gsumlsscl  48341  ldepspr  48435  lincresunit3lem3  48436  lincresunit3lem1  48441  lincresunit3  48443  reorelicc  48672  itsclc0yqsol  48726  itsclc0  48733