Theorem 3simpa 1051

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
3simpa	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

Proof of Theorem 3simpa

Step	Hyp	Ref	Expression
1		df-3an 1033	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2	1	simplbi 475	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3simpb  1052  3simpc  1053  simp1  1054  simp2  1055  3adant3  1074  3adantl3  1212  3adantr3  1215  otel3xp  5077  brcogw  5212  funtpg  5856  funtpgOLD  5857  ftpg  6328  ovig  6680  el2xptp0  7103  wfrlem17  7318  undifixp  7830  tz9.1c  8489  ackbij1lem16  8940  enqeq  9635  prlem934  9734  lt2halves  11144  nn0n0n1ge2  11235  ixxssixx  12060  ltdifltdiv  12497  hash2prd  13114  hashtpg  13121  2swrdeqwrdeq  13305  swrd0swrd0  13315  swrdccatid  13348  sumtp  14322  dvdscmulr  14848  dvdsmulcr  14849  dvds2add  14853  dvds2sub  14854  dvdstr  14856  vdwlem12  15534  cshwsidrepswmod0  15639  cshwshashlem2  15641  setsstruct  15727  initoeu2lem0  16486  estrreslem1  16600  funcestrcsetclem9  16611  funcsetcestrclem9  16626  sgrp2nmndlem4  17238  dfgrp3e  17338  lmhmlem  18850  psgndiflemA  19766  mpt2frlmd  19935  matsc  20075  scmatrhmcl  20153  mdetdiaglem  20223  decpmatid  20394  decpmatmullem  20395  mp2pm2mplem4  20433  chfacfisf  20478  chfacfisfcpmat  20479  cpmidgsumm2pm  20493  cpmidpmat  20497  cpmadumatpoly  20507  2ndcctbss  21068  dvfsumrlim  23598  dvfsumrlim2  23599  ulmval  23938  relogbmul  24315  axcontlem2  25645  funvtxval  25695  funiedgval  25696  cusgra2v  25991  2mwlk  26049  wlkelwrd  26058  constr3lem4  26175  constr3trllem2  26179  constr3trllem3  26180  wlkiswwlk2  26225  wwlknimpb  26232  clwwisshclww  26335  frg2woteq  26587  numclwwlk5  26639  leopmul  28377  strlem3a  28495  0elsiga  29504  afsval  30002  bnj999  30281  cgr3permute3  31324  cgr3com  31330  colineardim1  31338  brofs2  31354  brifs2  31355  btwnconn1lem4  31367  btwnconn1lem5  31368  btwnconn1lem6  31369  midofsegid  31381  isbasisrelowllem1  32379  isbasisrelowllem2  32380  icoreclin  32381  ftc1anclem8  32662  sdclem2  32708  ismndo1  32842  lsmcv2  33334  lvolnleat  33887  paddasslem14  34137  4atexlemswapqr  34367  isltrn2N  34424  cdlemftr1  34873  cdlemg5  34911  iocinico  36816  pwinfi2  36886  relexpxpnnidm  37014  sigaras  39693  sigarms  39694  bgoldbtbndlem4  40224  bgoldbtbnd  40225  pfxsuffeqwrdeq  40269  pfxccatpfx1  40290  pfxccatpfx2  40291  pr1eqbg  40313  uspgr1v1eop  40475  uhgrissubgr  40499  subgrprop3  40500  0uhgrsubgr  40503  2m1wlk  40818  1wlkelwrd  40837  uhgr1wlkspth  40961  usgr2wlkspth  40965  wwlknbp2  41063  2pthon3v-av  41150  uhgr3cyclex  41349  umgr3v3e3cycl  41351  av-numclwwlk5  41542  mhmismgmhm  41596  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859  gsumlsscl  41958  ldepspr  42056  lincresunit3lem3  42057  lincresunit3lem1  42062  lincresunit3  42064