Theorem 3simpa 1149

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3adantl3  1170  3adantr3  1173  disjtp2  4660  pr1eqbg  4800  preq12nebg  4806  otel3xp  5677  brcogw  5823  funtpg  6553  ftpg  7110  ovig  7513  el2xptp0  7989  fprresex  8260  undifixp  8882  tz9.1c  9651  ackbij1lem16  10156  enqeq  10857  prlem934  10956  lt2halves  12412  nn0n0n1ge2  12505  ixxssixx  13312  ltdifltdiv  13793  hash2prd  14437  hashtpg  14447  pfxsuffeqwrdeq  14660  pfxccatpfx1  14698  pfxccatpfx2  14699  s3eq3seq  14901  sumtp  15711  dvdscmulr  16253  dvdsmulcr  16254  dvds2add  16259  dvds2sub  16260  dvdstr  16263  vdwlem12  16963  cshwsidrepswmod0  17065  cshwshashlem2  17067  initoeu2lem0  17980  estrreslem1  18103  funcestrcsetclem9  18114  funcsetcestrclem9  18129  mhmismgmhm  18759  resmndismnd  18776  sgrp2nmndlem4  18899  dfgrp3e  19016  lmhmlem  21024  cnfldfunALT  21367  psgndiflemA  21581  matsc  22415  scmatrhmcl  22493  mdetdiaglem  22563  decpmatid  22735  decpmatmullem  22736  mp2pm2mplem4  22774  chfacfisf  22819  chfacfisfcpmat  22820  cpmidgsumm2pm  22834  cpmidpmat  22838  cpmadumatpoly  22848  2ndcctbss  23420  dvfsumrlim  25998  dvfsumrlim2  25999  ulmval  26345  relogbmul  26741  conway  27771  axcontlem2  29034  uspgr1v1eop  29318  uhgrissubgr  29344  subgrprop3  29345  0uhgrsubgr  29348  wlkelwrd  29701  uhgrwkspth  29823  usgr2wlkspth  29827  2pthon3v  30011  uhgr3cyclex  30252  umgr3v3e3cycl  30254  numclwwlk1lem2foa  30424  numclwwlk5  30458  leopmul  32205  strlem3a  32323  0elsiga  34258  afsval  34815  bnj999  35100  axprALT2  35253  tz9.1regs  35278  subgrwlk  35314  cusgr3cyclex  35318  acycgrislfgr  35334  satfvsucsuc  35547  ex-sategoelel  35603  ex-sategoel  35604  cgr3permute3  36229  cgr3com  36235  colineardim1  36243  brofs2  36259  brifs2  36260  btwnconn1lem4  36272  btwnconn1lem5  36273  btwnconn1lem6  36274  midofsegid  36286  ttcexg  36714  isbasisrelowllem1  37671  isbasisrelowllem2  37672  icoreclin  37673  ftc1anclem8  38021  sdclem2  38063  ismndo1  38194  refrelredund2  39041  lsmcv2  39475  lvolnleat  40029  paddasslem14  40279  4atexlemswapqr  40509  isltrn2N  40566  cdlemftr1  41013  cdlemg5  41051  iocinico  43640  omge1  43725  pwinfi2  43989  relexpxpnnidm  44130  pimxrneun  45916  sigaras  47283  sigarms  47284  difltmodne  47796  even3prm2  48195  fpprwpprb  48216  bgoldbtbndlem4  48284  bgoldbtbnd  48285  predgclnbgrel  48315  uhgrimprop  48368  grimgrtri  48425  grlimgrtri  48479  funcringcsetcALTV2lem9  48774  funcringcsetclem9ALTV  48797  fprmappr  48821  gsumlsscl  48856  ldepspr  48949  lincresunit3lem3  48950  lincresunit3lem1  48955  lincresunit3  48957  reorelicc  49186  itsclc0yqsol  49240  itsclc0  49247