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  4677  pr1eqbg  4817  preq12nebg  4823  otel3xp  5697  brcogw  5846  funtpg  6593  ftpg  7158  ovig  7564  el2xptp0  8045  fprresex  8321  undifixp  8955  tz9.1c  9724  ackbij1lem16  10305  enqeq  11012  prlem934  11111  lt2halves  12574  nn0n0n1ge2  12667  ixxssixx  13483  ltdifltdiv  13967  hash2prd  14613  hashtpg  14623  pfxsuffeqwrdeq  14840  pfxccatpfx1  14878  pfxccatpfx2  14879  s3eq3seq  15083  sumtp  15908  dvdscmulr  16447  dvdsmulcr  16448  dvds2add  16453  dvds2sub  16454  dvdstr  16457  vdwlem12  17163  cshwsidrepswmod0  17265  cshwshashlem2  17267  initoeu2lem0  18181  estrreslem1  18304  funcestrcsetclem9  18315  funcsetcestrclem9  18330  mhmismgmhm  18979  resmndismnd  18996  sgrp2nmndlem4  19120  dfgrp3e  19243  lmhmlem  21297  cnfldfunALT  21686  psgndiflemA  21900  matsc  22758  scmatrhmcl  22836  mdetdiaglem  22906  decpmatid  23081  decpmatmullem  23082  mp2pm2mplem4  23120  chfacfisf  23165  chfacfisfcpmat  23166  cpmidgsumm2pm  23180  cpmidpmat  23184  cpmadumatpoly  23194  2ndcctbss  23767  dvfsumrlim  26344  dvfsumrlim2  26345  ulmval  26700  relogbmul  27098  conway  28158  axcontlem2  29536  uspgr1v1eop  29823  uhgrissubgr  29849  subgrprop3  29850  0uhgrsubgr  29853  wlkelwrd  30206  subgrwlk  30262  uhgrwkspth  30334  usgr2wlkspth  30338  2pthon3v  30525  uhgr3cyclex  30776  umgr3v3e3cycl  30778  numclwwlk1lem2foa  30948  numclwwlk5  30982  leopmul  32729  strlem3a  32847  0elsiga  34739  afsval  35296  bnj999  35581  axprALT2  35723  tz9.1regs  35785  cusgr3cyclex  35890  acycgrislfgr  35896  satfvsucsuc  36109  ex-sategoelel  36165  ex-sategoel  36166  cgr3permute3  36792  cgr3com  36798  colineardim1  36806  brofs2  36822  brifs2  36823  btwnconn1lem4  36835  btwnconn1lem5  36836  btwnconn1lem6  36837  midofsegid  36849  ttcexg  37300  isbasisrelowllem1  38258  isbasisrelowllem2  38259  icoreclin  38260  ftc1anclem8  38598  sdclem2  38656  ismndo1  38787  refrelredund2  39632  lsmcv2  40066  lvolnleat  40620  paddasslem14  40870  4atexlemswapqr  41100  isltrn2N  41157  cdlemftr1  41604  cdlemg5  41642  iocinico  44198  omge1  44283  pwinfi2  44547  relexpxpnnidm  44688  pimxrneun  46467  sigaras  47834  sigarms  47835  difltmodne  48387  even3prm2  48786  fpprwpprb  48807  bgoldbtbndlem4  48875  bgoldbtbnd  48876  predgclnbgrel  48906  uhgrimprop  48959  grimgrtri  49016  grlimgrtri  49070  funcringcsetcALTV2lem9  49364  funcringcsetclem9ALTV  49387  fprmappr  49426  gsumlsscl  49461  ldepspr  49554  lincresunit3lem3  49555  lincresunit3lem1  49560  lincresunit3  49562  reorelicc  49791  itsclc0yqsol  49845  itsclc0  49852