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  4673  pr1eqbg  4811  preq12nebg  4817  otel3xp  5697  brcogw  5847  funtpg  6600  ftpg  7165  ovig  7570  el2xptp0  8051  fprresex  8335  undifixp  8969  tz9.1c  9738  ackbij1lem16  10319  enqeq  11026  prlem934  11125  lt2halves  12588  nn0n0n1ge2  12681  ixxssixx  13497  ltdifltdiv  13981  hash2prd  14627  hashtpg  14637  pfxsuffeqwrdeq  14855  pfxccatpfx1  14893  pfxccatpfx2  14894  s3eq3seq  15099  sumtp  15924  dvdscmulr  16463  dvdsmulcr  16464  dvds2add  16469  dvds2sub  16470  dvdstr  16473  vdwlem12  17179  cshwsidrepswmod0  17281  cshwshashlem2  17283  initoeu2lem0  18197  estrreslem1  18320  funcestrcsetclem9  18331  funcsetcestrclem9  18346  mhmismgmhm  18995  resmndismnd  19012  sgrp2nmndlem4  19136  dfgrp3e  19259  lmhmlem  21313  cnfldfunALT  21702  psgndiflemA  21916  matsc  22774  scmatrhmcl  22852  mdetdiaglem  22922  decpmatid  23097  decpmatmullem  23098  mp2pm2mplem4  23136  chfacfisf  23181  chfacfisfcpmat  23182  cpmidgsumm2pm  23196  cpmidpmat  23200  cpmadumatpoly  23210  2ndcctbss  23783  dvfsumrlim  26360  dvfsumrlim2  26361  ulmval  26716  relogbmul  27114  conway  28174  axcontlem2  29552  uspgr1v1eop  29839  uhgrissubgr  29865  subgrprop3  29866  0uhgrsubgr  29869  wlkelwrd  30222  subgrwlk  30278  uhgrwkspth  30350  usgr2wlkspth  30354  2pthon3v  30541  uhgr3cyclex  30792  umgr3v3e3cycl  30794  numclwwlk1lem2foa  30964  numclwwlk5  30998  leopmul  32745  strlem3a  32863  0elsiga  34796  afsval  35353  bnj999  35638  axprALT2  35790  tz9.1regs  35862  cusgr3cyclex  35991  acycgrislfgr  35997  satfvsucsuc  36220  ex-sategoelel  36276  ex-sategoel  36277  cgr3permute3  36908  cgr3com  36914  colineardim1  36922  brofs2  36938  brifs2  36939  btwnconn1lem4  36951  btwnconn1lem5  36952  btwnconn1lem6  36953  midofsegid  36965  ttcexg  37416  isbasisrelowllem1  38387  isbasisrelowllem2  38388  icoreclin  38389  ftc1anclem8  38727  sdclem2  38785  ismndo1  38916  refrelredund2  39761  lsmcv2  40195  lvolnleat  40749  paddasslem14  40999  4atexlemswapqr  41229  isltrn2N  41286  cdlemftr1  41733  cdlemg5  41771  iocinico  44323  omge1  44408  pwinfi2  44672  relexpxpnnidm  44812  pimxrneun  46606  sigaras  47973  sigarms  47974  difltmodne  48526  even3prm2  48925  fpprwpprb  48946  bgoldbtbndlem4  49014  bgoldbtbnd  49015  predgclnbgrel  49045  uhgrimprop  49098  grimgrtri  49155  grlimgrtri  49209  funcringcsetcALTV2lem9  49503  funcringcsetclem9ALTV  49526  fprmappr  49565  gsumlsscl  49600  ldepspr  49693  lincresunit3lem3  49694  lincresunit3lem1  49699  lincresunit3  49701  reorelicc  49930  itsclc0yqsol  49984  itsclc0  49991