Theorem 3simpa 1145

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3adantl3  1165  3adantr3  1168  disjtp2  4609  pr1eqbg  4744  preq12nebg  4750  otel3xp  5568  brcogw  5708  funtpg  6390  ftpg  6909  ovig  7291  el2xptp0  7740  wfrlem17  7981  undifixp  8516  tz9.1c  9205  ackbij1lem16  9695  enqeq  10394  prlem934  10493  lt2halves  11909  nn0n0n1ge2  12001  ixxssixx  12793  ltdifltdiv  13253  hash2prd  13885  hashtpg  13895  pfxsuffeqwrdeq  14107  pfxccatpfx1  14145  pfxccatpfx2  14146  s3eq3seq  14348  sumtp  15152  dvdscmulr  15686  dvdsmulcr  15687  dvds2add  15691  dvds2sub  15692  dvdstr  15695  vdwlem12  16383  cshwsidrepswmod0  16486  cshwshashlem2  16488  initoeu2lem0  17339  estrreslem1  17453  funcestrcsetclem9  17464  funcsetcestrclem9  17479  resmndismnd  18039  sgrp2nmndlem4  18159  dfgrp3e  18266  lmhmlem  19869  psgndiflemA  20366  matsc  21150  scmatrhmcl  21228  mdetdiaglem  21298  decpmatid  21470  decpmatmullem  21471  mp2pm2mplem4  21509  chfacfisf  21554  chfacfisfcpmat  21555  cpmidgsumm2pm  21569  cpmidpmat  21573  cpmadumatpoly  21583  2ndcctbss  22155  dvfsumrlim  24730  dvfsumrlim2  24731  ulmval  25074  relogbmul  25462  axcontlem2  26858  uspgr1v1eop  27138  uhgrissubgr  27164  subgrprop3  27165  0uhgrsubgr  27168  wlkelwrd  27521  uhgrwkspth  27643  usgr2wlkspth  27647  2pthon3v  27828  uhgr3cyclex  28066  umgr3v3e3cycl  28068  numclwwlk1lem2foa  28238  numclwwlk5  28272  leopmul  30016  strlem3a  30134  0elsiga  31601  afsval  32170  bnj999  32458  subgrwlk  32610  cusgr3cyclex  32614  acycgrislfgr  32630  satfvsucsuc  32843  ex-sategoelel  32899  ex-sategoel  32900  conway  33556  cgr3permute3  33898  cgr3com  33904  colineardim1  33912  brofs2  33928  brifs2  33929  btwnconn1lem4  33941  btwnconn1lem5  33942  btwnconn1lem6  33943  midofsegid  33955  isbasisrelowllem1  35052  isbasisrelowllem2  35053  icoreclin  35054  ftc1anclem8  35417  sdclem2  35460  ismndo1  35591  refrelredund2  36311  lsmcv2  36605  lvolnleat  37159  paddasslem14  37409  4atexlemswapqr  37639  isltrn2N  37696  cdlemftr1  38143  cdlemg5  38181  iocinico  40535  pwinfi2  40634  relexpxpnnidm  40777  sigaras  43835  sigarms  43836  even3prm2  44604  fpprwpprb  44625  bgoldbtbndlem4  44693  bgoldbtbnd  44694  mhmismgmhm  44793  funcringcsetcALTV2lem9  45035  funcringcsetclem9ALTV  45058  fprmappr  45114  gsumlsscl  45152  ldepspr  45247  lincresunit3lem3  45248  lincresunit3lem1  45253  lincresunit3  45255  reorelicc  45489  itsclc0yqsol  45543  itsclc0  45550