Theorem 3simpa 1146

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

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

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 396  df-3an 1087

This theorem is referenced by:  3adantl3  1166  3adantr3  1169  disjtp2  4649  pr1eqbg  4784  preq12nebg  4790  otel3xp  5624  brcogw  5766  funtpg  6473  ftpg  7010  ovig  7397  el2xptp0  7851  fprresex  8097  wfrlem17OLD  8127  undifixp  8680  tz9.1c  9419  ackbij1lem16  9922  enqeq  10621  prlem934  10720  lt2halves  12138  nn0n0n1ge2  12230  ixxssixx  13022  ltdifltdiv  13482  hash2prd  14117  hashtpg  14127  pfxsuffeqwrdeq  14339  pfxccatpfx1  14377  pfxccatpfx2  14378  s3eq3seq  14580  sumtp  15389  dvdscmulr  15922  dvdsmulcr  15923  dvds2add  15927  dvds2sub  15928  dvdstr  15931  vdwlem12  16621  cshwsidrepswmod0  16724  cshwshashlem2  16726  initoeu2lem0  17644  estrreslem1  17769  estrreslem1OLD  17770  funcestrcsetclem9  17781  funcsetcestrclem9  17796  resmndismnd  18362  sgrp2nmndlem4  18482  dfgrp3e  18590  lmhmlem  20206  psgndiflemA  20718  matsc  21507  scmatrhmcl  21585  mdetdiaglem  21655  decpmatid  21827  decpmatmullem  21828  mp2pm2mplem4  21866  chfacfisf  21911  chfacfisfcpmat  21912  cpmidgsumm2pm  21926  cpmidpmat  21930  cpmadumatpoly  21940  2ndcctbss  22514  dvfsumrlim  25100  dvfsumrlim2  25101  ulmval  25444  relogbmul  25832  axcontlem2  27236  uspgr1v1eop  27519  uhgrissubgr  27545  subgrprop3  27546  0uhgrsubgr  27549  wlkelwrd  27902  uhgrwkspth  28024  usgr2wlkspth  28028  2pthon3v  28209  uhgr3cyclex  28447  umgr3v3e3cycl  28449  numclwwlk1lem2foa  28619  numclwwlk5  28653  leopmul  30397  strlem3a  30515  0elsiga  31982  afsval  32551  bnj999  32838  subgrwlk  32994  cusgr3cyclex  32998  acycgrislfgr  33014  satfvsucsuc  33227  ex-sategoelel  33283  ex-sategoel  33284  conway  33920  cgr3permute3  34276  cgr3com  34282  colineardim1  34290  brofs2  34306  brifs2  34307  btwnconn1lem4  34319  btwnconn1lem5  34320  btwnconn1lem6  34321  midofsegid  34333  isbasisrelowllem1  35453  isbasisrelowllem2  35454  icoreclin  35455  ftc1anclem8  35784  sdclem2  35827  ismndo1  35958  refrelredund2  36676  lsmcv2  36970  lvolnleat  37524  paddasslem14  37774  4atexlemswapqr  38004  isltrn2N  38061  cdlemftr1  38508  cdlemg5  38546  iocinico  40959  pwinfi2  41058  relexpxpnnidm  41200  sigaras  44258  sigarms  44259  even3prm2  45059  fpprwpprb  45080  bgoldbtbndlem4  45148  bgoldbtbnd  45149  mhmismgmhm  45248  funcringcsetcALTV2lem9  45490  funcringcsetclem9ALTV  45513  fprmappr  45569  gsumlsscl  45607  ldepspr  45702  lincresunit3lem3  45703  lincresunit3lem1  45708  lincresunit3  45710  reorelicc  45944  itsclc0yqsol  45998  itsclc0  46005