Theorem 3simpa 1166

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 23	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2	1	3adant3 1150	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3adantl3  1187  3adantr3  1190  disjtp2  4682  pr1eqbg  4822  preq12nebg  4828  otel3xp  5707  brcogw  5854  funtpg  6591  ftpg  7153  ovig  7556  el2xptp0  8029  fprresex  8303  undifixp  8928  tz9.1c  9695  ackbij1lem16  10213  enqeq  10914  prlem934  11013  lt2halves  12474  nn0n0n1ge2  12567  ixxssixx  13381  ltdifltdiv  13863  hash2prd  14508  hashtpg  14518  pfxsuffeqwrdeq  14731  pfxccatpfx1  14769  pfxccatpfx2  14770  s3eq3seq  14972  sumtp  15796  dvdscmulr  16337  dvdsmulcr  16338  dvds2add  16343  dvds2sub  16344  dvdstr  16347  vdwlem12  17047  cshwsidrepswmod0  17149  cshwshashlem2  17151  initoeu2lem0  18065  estrreslem1  18188  funcestrcsetclem9  18199  funcsetcestrclem9  18214  mhmismgmhm  18844  resmndismnd  18861  sgrp2nmndlem4  18985  dfgrp3e  19101  lmhmlem  21150  cnfldfunALT  21537  psgndiflemA  21751  matsc  22607  scmatrhmcl  22685  mdetdiaglem  22755  decpmatid  22927  decpmatmullem  22928  mp2pm2mplem4  22966  chfacfisf  23011  chfacfisfcpmat  23012  cpmidgsumm2pm  23026  cpmidpmat  23030  cpmadumatpoly  23040  2ndcctbss  23612  dvfsumrlim  26190  dvfsumrlim2  26191  ulmval  26543  relogbmul  26942  conway  27972  axcontlem2  29315  uspgr1v1eop  29599  uhgrissubgr  29625  subgrprop3  29626  0uhgrsubgr  29629  wlkelwrd  29982  uhgrwkspth  30104  usgr2wlkspth  30108  2pthon3v  30292  uhgr3cyclex  30533  umgr3v3e3cycl  30535  numclwwlk1lem2foa  30705  numclwwlk5  30739  leopmul  32486  strlem3a  32604  0elsiga  34504  afsval  35061  bnj999  35346  axprALT2  35503  tz9.1regs  35547  subgrwlk  35624  cusgr3cyclex  35628  acycgrislfgr  35644  satfvsucsuc  35857  ex-sategoelel  35913  ex-sategoel  35914  cgr3permute3  36539  cgr3com  36545  colineardim1  36553  brofs2  36569  brifs2  36570  btwnconn1lem4  36582  btwnconn1lem5  36583  btwnconn1lem6  36584  midofsegid  36596  ttcexg  37043  isbasisrelowllem1  38001  isbasisrelowllem2  38002  icoreclin  38003  ftc1anclem8  38351  sdclem2  38393  ismndo1  38524  refrelredund2  39369  lsmcv2  39803  lvolnleat  40357  paddasslem14  40607  4atexlemswapqr  40837  isltrn2N  40894  cdlemftr1  41341  cdlemg5  41379  iocinico  43939  omge1  44024  pwinfi2  44288  relexpxpnnidm  44429  pimxrneun  46202  sigaras  47569  sigarms  47570  difltmodne  48085  even3prm2  48484  fpprwpprb  48505  bgoldbtbndlem4  48573  bgoldbtbnd  48574  predgclnbgrel  48604  uhgrimprop  48657  grimgrtri  48714  grlimgrtri  48768  funcringcsetcALTV2lem9  49063  funcringcsetclem9ALTV  49086  fprmappr  49125  gsumlsscl  49160  ldepspr  49253  lincresunit3lem3  49254  lincresunit3lem1  49259  lincresunit3  49261  reorelicc  49490  itsclc0yqsol  49544  itsclc0  49551