Theorem 3simpa 1154

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3adantl3  1175  3adantr3  1178  disjtp2  4648  pr1eqbg  4788  preq12nebg  4794  otel3xp  5664  brcogw  5810  funtpg  6540  ftpg  7099  ovig  7502  el2xptp0  7978  fprresex  8250  undifixp  8872  tz9.1c  9642  ackbij1lem16  10147  enqeq  10848  prlem934  10947  lt2halves  12403  nn0n0n1ge2  12496  ixxssixx  13303  ltdifltdiv  13784  hash2prd  14428  hashtpg  14438  pfxsuffeqwrdeq  14651  pfxccatpfx1  14689  pfxccatpfx2  14690  s3eq3seq  14892  sumtp  15702  dvdscmulr  16244  dvdsmulcr  16245  dvds2add  16250  dvds2sub  16251  dvdstr  16254  vdwlem12  16954  cshwsidrepswmod0  17056  cshwshashlem2  17058  initoeu2lem0  17971  estrreslem1  18094  funcestrcsetclem9  18105  funcsetcestrclem9  18120  mhmismgmhm  18750  resmndismnd  18767  sgrp2nmndlem4  18890  dfgrp3e  19007  lmhmlem  21019  cnfldfunALT  21362  psgndiflemA  21576  matsc  22433  scmatrhmcl  22511  mdetdiaglem  22581  decpmatid  22753  decpmatmullem  22754  mp2pm2mplem4  22792  chfacfisf  22837  chfacfisfcpmat  22838  cpmidgsumm2pm  22852  cpmidpmat  22856  cpmadumatpoly  22866  2ndcctbss  23438  dvfsumrlim  26016  dvfsumrlim2  26017  ulmval  26363  relogbmul  26759  conway  27789  axcontlem2  29052  uspgr1v1eop  29336  uhgrissubgr  29362  subgrprop3  29363  0uhgrsubgr  29366  wlkelwrd  29719  uhgrwkspth  29841  usgr2wlkspth  29845  2pthon3v  30029  uhgr3cyclex  30270  umgr3v3e3cycl  30272  numclwwlk1lem2foa  30442  numclwwlk5  30476  leopmul  32223  strlem3a  32341  0elsiga  34298  afsval  34855  bnj999  35140  axprALT2  35290  tz9.1regs  35315  subgrwlk  35360  cusgr3cyclex  35364  acycgrislfgr  35380  satfvsucsuc  35593  ex-sategoelel  35649  ex-sategoel  35650  cgr3permute3  36275  cgr3com  36281  colineardim1  36289  brofs2  36305  brifs2  36306  btwnconn1lem4  36318  btwnconn1lem5  36319  btwnconn1lem6  36320  midofsegid  36332  ttcexg  36760  isbasisrelowllem1  37717  isbasisrelowllem2  37718  icoreclin  37719  ftc1anclem8  38067  sdclem2  38109  ismndo1  38240  refrelredund2  39087  lsmcv2  39521  lvolnleat  40075  paddasslem14  40325  4atexlemswapqr  40555  isltrn2N  40612  cdlemftr1  41059  cdlemg5  41097  iocinico  43657  omge1  43742  pwinfi2  44006  relexpxpnnidm  44147  pimxrneun  45931  sigaras  47298  sigarms  47299  difltmodne  47811  even3prm2  48210  fpprwpprb  48231  bgoldbtbndlem4  48299  bgoldbtbnd  48300  predgclnbgrel  48330  uhgrimprop  48383  grimgrtri  48440  grlimgrtri  48494  funcringcsetcALTV2lem9  48789  funcringcsetclem9ALTV  48812  fprmappr  48836  gsumlsscl  48871  ldepspr  48964  lincresunit3lem3  48965  lincresunit3lem1  48970  lincresunit3  48972  reorelicc  49201  itsclc0yqsol  49255  itsclc0  49262