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 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3adantl3  1169  3adantr3  1172  disjtp2  4716  pr1eqbg  4853  preq12nebg  4859  otel3xp  5717  brcogw  5863  funtpg  6595  ftpg  7141  ovig  7541  el2xptp0  8009  fprresex  8282  wfrlem17OLD  8312  undifixp  8916  tz9.1c  9712  ackbij1lem16  10217  enqeq  10916  prlem934  11015  lt2halves  12434  nn0n0n1ge2  12526  ixxssixx  13325  ltdifltdiv  13786  hash2prd  14423  hashtpg  14433  pfxsuffeqwrdeq  14635  pfxccatpfx1  14673  pfxccatpfx2  14674  s3eq3seq  14877  sumtp  15682  dvdscmulr  16215  dvdsmulcr  16216  dvds2add  16220  dvds2sub  16221  dvdstr  16224  vdwlem12  16912  cshwsidrepswmod0  17015  cshwshashlem2  17017  initoeu2lem0  17950  estrreslem1  18075  estrreslem1OLD  18076  funcestrcsetclem9  18087  funcsetcestrclem9  18102  resmndismnd  18676  sgrp2nmndlem4  18796  dfgrp3e  18910  lmhmlem  20617  cnfldfunALT  20931  psgndiflemA  21127  matsc  21921  scmatrhmcl  21999  mdetdiaglem  22069  decpmatid  22241  decpmatmullem  22242  mp2pm2mplem4  22280  chfacfisf  22325  chfacfisfcpmat  22326  cpmidgsumm2pm  22340  cpmidpmat  22344  cpmadumatpoly  22354  2ndcctbss  22928  dvfsumrlim  25517  dvfsumrlim2  25518  ulmval  25861  relogbmul  26249  conway  27267  axcontlem2  28190  uspgr1v1eop  28473  uhgrissubgr  28499  subgrprop3  28500  0uhgrsubgr  28503  wlkelwrd  28857  uhgrwkspth  28979  usgr2wlkspth  28983  2pthon3v  29164  uhgr3cyclex  29402  umgr3v3e3cycl  29404  numclwwlk1lem2foa  29574  numclwwlk5  29608  leopmul  31352  strlem3a  31470  0elsiga  33043  afsval  33614  bnj999  33900  subgrwlk  34054  cusgr3cyclex  34058  acycgrislfgr  34074  satfvsucsuc  34287  ex-sategoelel  34343  ex-sategoel  34344  cgr3permute3  34950  cgr3com  34956  colineardim1  34964  brofs2  34980  brifs2  34981  btwnconn1lem4  34993  btwnconn1lem5  34994  btwnconn1lem6  34995  midofsegid  35007  isbasisrelowllem1  36141  isbasisrelowllem2  36142  icoreclin  36143  ftc1anclem8  36473  sdclem2  36516  ismndo1  36647  refrelredund2  37412  lsmcv2  37805  lvolnleat  38360  paddasslem14  38610  4atexlemswapqr  38840  isltrn2N  38897  cdlemftr1  39344  cdlemg5  39382  iocinico  41832  omge1  41918  pwinfi2  42184  relexpxpnnidm  42325  pimxrneun  44072  sigaras  45444  sigarms  45445  even3prm2  46260  fpprwpprb  46281  bgoldbtbndlem4  46349  bgoldbtbnd  46350  mhmismgmhm  46449  funcringcsetcALTV2lem9  46782  funcringcsetclem9ALTV  46805  fprmappr  46861  gsumlsscl  46899  ldepspr  46994  lincresunit3lem3  46995  lincresunit3lem1  47000  lincresunit3  47002  reorelicc  47236  itsclc0yqsol  47290  itsclc0  47297