Theorem 3simpa 1058

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 1039	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2	1	simplbi 476	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3simpb  1059  3simpc  1060  simp1  1061  simp2  1062  3adant3  1081  3adantl3  1219  3adantr3  1222  disjtp2  4252  pr1eqbg  4390  otel3xp  5153  brcogw  5290  funtpg  5942  funtpgOLD  5943  ftpg  6423  ovig  6782  el2xptp0  7212  wfrlem17  7431  undifixp  7944  tz9.1c  8606  ackbij1lem16  9057  enqeq  9756  prlem934  9855  lt2halves  11267  nn0n0n1ge2  11358  ixxssixx  12189  ltdifltdiv  12635  hash2prd  13257  hashtpg  13267  2swrdeqwrdeq  13453  swrd0swrd0  13463  swrdccatid  13497  s3eq3seq  13684  sumtp  14478  dvdscmulr  15010  dvdsmulcr  15011  dvds2add  15015  dvds2sub  15016  dvdstr  15018  vdwlem12  15696  cshwsidrepswmod0  15801  cshwshashlem2  15803  setsstructOLD  15899  initoeu2lem0  16663  estrreslem1  16777  funcestrcsetclem9  16788  funcsetcestrclem9  16803  sgrp2nmndlem4  17415  dfgrp3e  17515  lmhmlem  19029  psgndiflemA  19947  mpt2frlmd  20116  matsc  20256  scmatrhmcl  20334  mdetdiaglem  20404  decpmatid  20575  decpmatmullem  20576  mp2pm2mplem4  20614  chfacfisf  20659  chfacfisfcpmat  20660  cpmidgsumm2pm  20674  cpmidpmat  20678  cpmadumatpoly  20688  2ndcctbss  21258  dvfsumrlim  23794  dvfsumrlim2  23795  ulmval  24134  relogbmul  24515  axcontlem2  25845  funvtxvalOLD  25907  funiedgvalOLD  25908  uspgr1v1eop  26141  uhgrissubgr  26167  subgrprop3  26168  0uhgrsubgr  26171  wlkelwrd  26528  uhgrwkspth  26651  usgr2wlkspth  26655  wwlknbp2  26752  2pthon3v  26839  uhgr3cyclex  27042  umgr3v3e3cycl  27044  numclwwlk5  27246  leopmul  28993  strlem3a  29111  0elsiga  30177  afsval  30749  bnj999  31027  conway  31910  cgr3permute3  32154  cgr3com  32160  colineardim1  32168  brofs2  32184  brifs2  32185  btwnconn1lem4  32197  btwnconn1lem5  32198  btwnconn1lem6  32199  midofsegid  32211  isbasisrelowllem1  33203  isbasisrelowllem2  33204  icoreclin  33205  ftc1anclem8  33492  sdclem2  33538  ismndo1  33672  lsmcv2  34316  lvolnleat  34869  paddasslem14  35119  4atexlemswapqr  35349  isltrn2N  35406  cdlemftr1  35855  cdlemg5  35893  iocinico  37797  pwinfi2  37867  relexpxpnnidm  37995  sigaras  41044  sigarms  41045  pfxsuffeqwrdeq  41406  pfxccatpfx1  41427  pfxccatpfx2  41428  even3prm2  41628  bgoldbtbndlem4  41696  bgoldbtbnd  41697  mhmismgmhm  41806  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067  gsumlsscl  42164  ldepspr  42262  lincresunit3lem3  42263  lincresunit3lem1  42268  lincresunit3  42270