Theorem 3simpa 1144

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3adantl3  1164  3adantr3  1167  disjtp2  4645  pr1eqbg  4780  preq12nebg  4786  otel3xp  5593  brcogw  5733  funtpg  6403  ftpg  6912  ovig  7290  el2xptp0  7730  wfrlem17  7965  undifixp  8492  tz9.1c  9166  ackbij1lem16  9651  enqeq  10350  prlem934  10449  lt2halves  11866  nn0n0n1ge2  11956  ixxssixx  12746  ltdifltdiv  13198  hash2prd  13827  hashtpg  13837  pfxsuffeqwrdeq  14054  pfxccatpfx1  14092  pfxccatpfx2  14093  s3eq3seq  14295  sumtp  15098  dvdscmulr  15632  dvdsmulcr  15633  dvds2add  15637  dvds2sub  15638  dvdstr  15640  vdwlem12  16322  cshwsidrepswmod0  16422  cshwshashlem2  16424  initoeu2lem0  17267  estrreslem1  17381  funcestrcsetclem9  17392  funcsetcestrclem9  17407  resmndismnd  17967  sgrp2nmndlem4  18087  dfgrp3e  18193  lmhmlem  19795  psgndiflemA  20739  matsc  21053  scmatrhmcl  21131  mdetdiaglem  21201  decpmatid  21372  decpmatmullem  21373  mp2pm2mplem4  21411  chfacfisf  21456  chfacfisfcpmat  21457  cpmidgsumm2pm  21471  cpmidpmat  21475  cpmadumatpoly  21485  2ndcctbss  22057  dvfsumrlim  24622  dvfsumrlim2  24623  ulmval  24962  relogbmul  25349  axcontlem2  26745  uspgr1v1eop  27025  uhgrissubgr  27051  subgrprop3  27052  0uhgrsubgr  27055  wlkelwrd  27408  uhgrwkspth  27530  usgr2wlkspth  27534  2pthon3v  27716  uhgr3cyclex  27955  umgr3v3e3cycl  27957  numclwwlk1lem2foa  28127  numclwwlk5  28161  leopmul  29905  strlem3a  30023  0elsiga  31368  afsval  31937  bnj999  32225  subgrwlk  32374  cusgr3cyclex  32378  acycgrislfgr  32394  satfvsucsuc  32607  ex-sategoelel  32663  ex-sategoel  32664  conway  33259  cgr3permute3  33503  cgr3com  33509  colineardim1  33517  brofs2  33533  brifs2  33534  btwnconn1lem4  33546  btwnconn1lem5  33547  btwnconn1lem6  33548  midofsegid  33560  isbasisrelowllem1  34630  isbasisrelowllem2  34631  icoreclin  34632  ftc1anclem8  34968  sdclem2  35011  ismndo1  35145  refrelredund2  35865  lsmcv2  36159  lvolnleat  36713  paddasslem14  36963  4atexlemswapqr  37193  isltrn2N  37250  cdlemftr1  37697  cdlemg5  37735  iocinico  39811  pwinfi2  39914  relexpxpnnidm  40041  sigaras  43106  sigarms  43107  even3prm2  43878  fpprwpprb  43899  bgoldbtbndlem4  43967  bgoldbtbnd  43968  mhmismgmhm  44067  funcringcsetcALTV2lem9  44309  funcringcsetclem9ALTV  44332  gsumlsscl  44425  ldepspr  44522  lincresunit3lem3  44523  lincresunit3lem1  44528  lincresunit3  44530  reorelicc  44691  itsclc0yqsol  44745  itsclc0  44752