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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adantl3  1187  3adantr3  1190  disjtp2  4679  pr1eqbg  4817  preq12nebg  4823  otel3xp  5704  brcogw  5857  funtpg  6625  ftpg  7192  ovig  7598  el2xptp0  8081  fprresex  8366  undifixp  9000  tz9.1c  9768  ackbij1lem16  10351  enqeq  11058  prlem934  11157  lt2halves  12621  nn0n0n1ge2  12714  ixxssixx  13530  ltdifltdiv  14014  hash2prd  14661  hashtpg  14671  pfxsuffeqwrdeq  14889  pfxccatpfx1  14927  pfxccatpfx2  14928  s3eq3seq  15133  sumtp  15959  dvdscmulr  16498  dvdsmulcr  16499  dvds2add  16504  dvds2sub  16505  dvdstr  16508  vdwlem12  17214  cshwsidrepswmod0  17316  cshwshashlem2  17318  initoeu2lem0  18238  estrreslem1  18361  funcestrcsetclem9  18372  funcsetcestrclem9  18387  mhmismgmhm  19036  resmndismnd  19053  sgrp2nmndlem4  19177  dfgrp3e  19300  lmhmlem  21355  cnfldfunALT  21745  psgndiflemA  21962  matsc  22820  scmatrhmcl  22898  mdetdiaglem  22968  decpmatid  23143  decpmatmullem  23144  mp2pm2mplem4  23182  chfacfisf  23227  chfacfisfcpmat  23228  cpmidgsumm2pm  23242  cpmidpmat  23246  cpmadumatpoly  23256  2ndcctbss  23829  dvfsumrlim  26406  dvfsumrlim2  26407  ulmval  26764  relogbmul  27162  conway  28222  axcontlem2  29600  uspgr1v1eop  29887  uhgrissubgr  29913  subgrprop3  29914  0uhgrsubgr  29917  wlkelwrd  30270  subgrwlk  30326  uhgrwkspth  30398  usgr2wlkspth  30402  2pthon3v  30589  uhgr3cyclex  30840  umgr3v3e3cycl  30842  numclwwlk1lem2foa  31012  numclwwlk5  31046  leopmul  32793  strlem3a  32911  0elsiga  34857  afsval  35414  bnj999  35699  axprALT2  35857  tz9.1regs  35943  cusgr3cyclex  36109  acycgrislfgr  36115  satfvsucsuc  36338  ex-sategoelel  36394  ex-sategoel  36395  cgr3permute3  37027  cgr3com  37033  colineardim1  37041  brofs2  37057  brifs2  37058  btwnconn1lem4  37070  btwnconn1lem5  37071  btwnconn1lem6  37072  midofsegid  37084  ttcexg  37535  isbasisrelowllem1  38546  isbasisrelowllem2  38547  icoreclin  38548  ftc1anclem8  38886  sdclem2  38942  ismndo1  39073  refrelredund2  39918  lsmcv2  40352  lvolnleat  40906  paddasslem14  41156  4atexlemswapqr  41386  isltrn2N  41443  cdlemftr1  41890  cdlemg5  41928  iocinico  44475  omge1  44560  pwinfi2  44824  relexpxpnnidm  44964  pimxrneun  46771  sigaras  48138  sigarms  48139  difltmodne  48691  even3prm2  49090  fpprwpprb  49111  bgoldbtbndlem4  49179  bgoldbtbnd  49180  predgclnbgrel  49210  uhgrimprop  49263  grimgrtri  49320  grlimgrtri  49374  funcringcsetcALTV2lem9  49668  funcringcsetclem9ALTV  49691  fprmappr  49788  gsumlsscl  49823  ldepspr  49916  lincresunit3lem3  49917  lincresunit3lem1  49922  lincresunit3  49924  reorelicc  50153  itsclc0yqsol  50207  itsclc0  50214