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  4668  pr1eqbg  4808  preq12nebg  4814  otel3xp  5665  brcogw  5811  funtpg  6537  ftpg  7090  ovig  7495  el2xptp0  7971  fprresex  8243  undifixp  8861  tz9.1c  9626  ackbij1lem16  10128  enqeq  10828  prlem934  10927  lt2halves  12359  nn0n0n1ge2  12452  ixxssixx  13262  ltdifltdiv  13738  hash2prd  14382  hashtpg  14392  pfxsuffeqwrdeq  14604  pfxccatpfx1  14642  pfxccatpfx2  14643  s3eq3seq  14846  sumtp  15656  dvdscmulr  16195  dvdsmulcr  16196  dvds2add  16201  dvds2sub  16202  dvdstr  16205  vdwlem12  16904  cshwsidrepswmod0  17006  cshwshashlem2  17008  initoeu2lem0  17920  estrreslem1  18043  funcestrcsetclem9  18054  funcsetcestrclem9  18069  mhmismgmhm  18665  resmndismnd  18682  sgrp2nmndlem4  18802  dfgrp3e  18919  lmhmlem  20933  cnfldfunALT  21276  cnfldfunALTOLD  21289  psgndiflemA  21508  matsc  22335  scmatrhmcl  22413  mdetdiaglem  22483  decpmatid  22655  decpmatmullem  22656  mp2pm2mplem4  22694  chfacfisf  22739  chfacfisfcpmat  22740  cpmidgsumm2pm  22754  cpmidpmat  22758  cpmadumatpoly  22768  2ndcctbss  23340  dvfsumrlim  25936  dvfsumrlim2  25937  ulmval  26287  relogbmul  26685  conway  27710  axcontlem2  28910  uspgr1v1eop  29194  uhgrissubgr  29220  subgrprop3  29221  0uhgrsubgr  29224  wlkelwrd  29578  uhgrwkspth  29700  usgr2wlkspth  29704  2pthon3v  29888  uhgr3cyclex  30126  umgr3v3e3cycl  30128  numclwwlk1lem2foa  30298  numclwwlk5  30332  leopmul  32078  strlem3a  32196  0elsiga  34081  afsval  34639  bnj999  34925  tz9.1regs  35067  subgrwlk  35105  cusgr3cyclex  35109  acycgrislfgr  35125  satfvsucsuc  35338  ex-sategoelel  35394  ex-sategoel  35395  cgr3permute3  36021  cgr3com  36027  colineardim1  36035  brofs2  36051  brifs2  36052  btwnconn1lem4  36064  btwnconn1lem5  36065  btwnconn1lem6  36066  midofsegid  36078  isbasisrelowllem1  37329  isbasisrelowllem2  37330  icoreclin  37331  ftc1anclem8  37680  sdclem2  37722  ismndo1  37853  refrelredund2  38613  lsmcv2  39008  lvolnleat  39562  paddasslem14  39812  4atexlemswapqr  40042  isltrn2N  40099  cdlemftr1  40546  cdlemg5  40584  iocinico  43185  omge1  43270  pwinfi2  43535  relexpxpnnidm  43676  pimxrneun  45467  sigaras  46836  sigarms  46837  difltmodne  47326  even3prm2  47703  fpprwpprb  47724  bgoldbtbndlem4  47792  bgoldbtbnd  47793  predgclnbgrel  47823  uhgrimprop  47876  grimgrtri  47933  grlimgrtri  47987  funcringcsetcALTV2lem9  48282  funcringcsetclem9ALTV  48305  fprmappr  48329  gsumlsscl  48364  ldepspr  48458  lincresunit3lem3  48459  lincresunit3lem1  48464  lincresunit3  48466  reorelicc  48695  itsclc0yqsol  48749  itsclc0  48756