Theorem 3simpa 1148

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

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

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

This theorem is referenced by:  3adantl3  1169  3adantr3  1172  disjtp2  4680  pr1eqbg  4821  preq12nebg  4827  otel3xp  5684  brcogw  5832  funtpg  6571  ftpg  7128  ovig  7535  el2xptp0  8015  fprresex  8289  undifixp  8907  tz9.1c  9683  ackbij1lem16  10187  enqeq  10887  prlem934  10986  lt2halves  12417  nn0n0n1ge2  12510  ixxssixx  13320  ltdifltdiv  13796  hash2prd  14440  hashtpg  14450  pfxsuffeqwrdeq  14663  pfxccatpfx1  14701  pfxccatpfx2  14702  s3eq3seq  14905  sumtp  15715  dvdscmulr  16254  dvdsmulcr  16255  dvds2add  16260  dvds2sub  16261  dvdstr  16264  vdwlem12  16963  cshwsidrepswmod0  17065  cshwshashlem2  17067  initoeu2lem0  17975  estrreslem1  18098  funcestrcsetclem9  18109  funcsetcestrclem9  18124  mhmismgmhm  18718  resmndismnd  18735  sgrp2nmndlem4  18855  dfgrp3e  18972  lmhmlem  20936  cnfldfunALT  21279  cnfldfunALTOLD  21292  psgndiflemA  21510  matsc  22337  scmatrhmcl  22415  mdetdiaglem  22485  decpmatid  22657  decpmatmullem  22658  mp2pm2mplem4  22696  chfacfisf  22741  chfacfisfcpmat  22742  cpmidgsumm2pm  22756  cpmidpmat  22760  cpmadumatpoly  22770  2ndcctbss  23342  dvfsumrlim  25938  dvfsumrlim2  25939  ulmval  26289  relogbmul  26687  conway  27711  axcontlem2  28892  uspgr1v1eop  29176  uhgrissubgr  29202  subgrprop3  29203  0uhgrsubgr  29206  wlkelwrd  29561  uhgrwkspth  29685  usgr2wlkspth  29689  2pthon3v  29873  uhgr3cyclex  30111  umgr3v3e3cycl  30113  numclwwlk1lem2foa  30283  numclwwlk5  30317  leopmul  32063  strlem3a  32181  0elsiga  34104  afsval  34662  bnj999  34948  subgrwlk  35119  cusgr3cyclex  35123  acycgrislfgr  35139  satfvsucsuc  35352  ex-sategoelel  35408  ex-sategoel  35409  cgr3permute3  36035  cgr3com  36041  colineardim1  36049  brofs2  36065  brifs2  36066  btwnconn1lem4  36078  btwnconn1lem5  36079  btwnconn1lem6  36080  midofsegid  36092  isbasisrelowllem1  37343  isbasisrelowllem2  37344  icoreclin  37345  ftc1anclem8  37694  sdclem2  37736  ismndo1  37867  refrelredund2  38627  lsmcv2  39022  lvolnleat  39577  paddasslem14  39827  4atexlemswapqr  40057  isltrn2N  40114  cdlemftr1  40561  cdlemg5  40599  iocinico  43201  omge1  43286  pwinfi2  43551  relexpxpnnidm  43692  pimxrneun  45484  sigaras  46853  sigarms  46854  difltmodne  47340  even3prm2  47717  fpprwpprb  47738  bgoldbtbndlem4  47806  bgoldbtbnd  47807  predgclnbgrel  47836  uhgrimprop  47889  grimgrtri  47945  grlimgrtri  47992  funcringcsetcALTV2lem9  48283  funcringcsetclem9ALTV  48306  fprmappr  48330  gsumlsscl  48365  ldepspr  48459  lincresunit3lem3  48460  lincresunit3lem1  48465  lincresunit3  48467  reorelicc  48696  itsclc0yqsol  48750  itsclc0  48757