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  4673  pr1eqbg  4813  preq12nebg  4819  otel3xp  5670  brcogw  5817  funtpg  6547  ftpg  7101  ovig  7504  el2xptp0  7980  fprresex  8252  undifixp  8872  tz9.1c  9639  ackbij1lem16  10144  enqeq  10845  prlem934  10944  lt2halves  12376  nn0n0n1ge2  12469  ixxssixx  13275  ltdifltdiv  13754  hash2prd  14398  hashtpg  14408  pfxsuffeqwrdeq  14621  pfxccatpfx1  14659  pfxccatpfx2  14660  s3eq3seq  14862  sumtp  15672  dvdscmulr  16211  dvdsmulcr  16212  dvds2add  16217  dvds2sub  16218  dvdstr  16221  vdwlem12  16920  cshwsidrepswmod0  17022  cshwshashlem2  17024  initoeu2lem0  17937  estrreslem1  18060  funcestrcsetclem9  18071  funcsetcestrclem9  18086  mhmismgmhm  18716  resmndismnd  18733  sgrp2nmndlem4  18853  dfgrp3e  18970  lmhmlem  20981  cnfldfunALT  21324  cnfldfunALTOLD  21337  psgndiflemA  21556  matsc  22394  scmatrhmcl  22472  mdetdiaglem  22542  decpmatid  22714  decpmatmullem  22715  mp2pm2mplem4  22753  chfacfisf  22798  chfacfisfcpmat  22799  cpmidgsumm2pm  22813  cpmidpmat  22817  cpmadumatpoly  22827  2ndcctbss  23399  dvfsumrlim  25994  dvfsumrlim2  25995  ulmval  26345  relogbmul  26743  conway  27775  axcontlem2  29038  uspgr1v1eop  29322  uhgrissubgr  29348  subgrprop3  29349  0uhgrsubgr  29352  wlkelwrd  29706  uhgrwkspth  29828  usgr2wlkspth  29832  2pthon3v  30016  uhgr3cyclex  30257  umgr3v3e3cycl  30259  numclwwlk1lem2foa  30429  numclwwlk5  30463  leopmul  32209  strlem3a  32327  0elsiga  34271  afsval  34828  bnj999  35114  tz9.1regs  35290  subgrwlk  35326  cusgr3cyclex  35330  acycgrislfgr  35346  satfvsucsuc  35559  ex-sategoelel  35615  ex-sategoel  35616  cgr3permute3  36241  cgr3com  36247  colineardim1  36255  brofs2  36271  brifs2  36272  btwnconn1lem4  36284  btwnconn1lem5  36285  btwnconn1lem6  36286  midofsegid  36298  isbasisrelowllem1  37560  isbasisrelowllem2  37561  icoreclin  37562  ftc1anclem8  37901  sdclem2  37943  ismndo1  38074  refrelredund2  38893  lsmcv2  39289  lvolnleat  39843  paddasslem14  40093  4atexlemswapqr  40323  isltrn2N  40380  cdlemftr1  40827  cdlemg5  40865  iocinico  43454  omge1  43539  pwinfi2  43803  relexpxpnnidm  43944  pimxrneun  45732  sigaras  47099  sigarms  47100  difltmodne  47588  even3prm2  47965  fpprwpprb  47986  bgoldbtbndlem4  48054  bgoldbtbnd  48055  predgclnbgrel  48085  uhgrimprop  48138  grimgrtri  48195  grlimgrtri  48249  funcringcsetcALTV2lem9  48544  funcringcsetclem9ALTV  48567  fprmappr  48591  gsumlsscl  48626  ldepspr  48719  lincresunit3lem3  48720  lincresunit3lem1  48725  lincresunit3  48727  reorelicc  48956  itsclc0yqsol  49010  itsclc0  49017