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  4612  pr1eqbg  4747  preq12nebg  4753  otel3xp  5563  brcogw  5703  funtpg  6379  ftpg  6895  ovig  7275  el2xptp0  7718  wfrlem17  7954  undifixp  8481  tz9.1c  9156  ackbij1lem16  9646  enqeq  10345  prlem934  10444  lt2halves  11860  nn0n0n1ge2  11950  ixxssixx  12740  ltdifltdiv  13199  hash2prd  13829  hashtpg  13839  pfxsuffeqwrdeq  14051  pfxccatpfx1  14089  pfxccatpfx2  14090  s3eq3seq  14292  sumtp  15096  dvdscmulr  15630  dvdsmulcr  15631  dvds2add  15635  dvds2sub  15636  dvdstr  15638  vdwlem12  16318  cshwsidrepswmod0  16420  cshwshashlem2  16422  initoeu2lem0  17265  estrreslem1  17379  funcestrcsetclem9  17390  funcsetcestrclem9  17405  resmndismnd  17965  sgrp2nmndlem4  18085  dfgrp3e  18191  lmhmlem  19794  psgndiflemA  20290  matsc  21055  scmatrhmcl  21133  mdetdiaglem  21203  decpmatid  21375  decpmatmullem  21376  mp2pm2mplem4  21414  chfacfisf  21459  chfacfisfcpmat  21460  cpmidgsumm2pm  21474  cpmidpmat  21478  cpmadumatpoly  21488  2ndcctbss  22060  dvfsumrlim  24634  dvfsumrlim2  24635  ulmval  24975  relogbmul  25363  axcontlem2  26759  uspgr1v1eop  27039  uhgrissubgr  27065  subgrprop3  27066  0uhgrsubgr  27069  wlkelwrd  27422  uhgrwkspth  27544  usgr2wlkspth  27548  2pthon3v  27729  uhgr3cyclex  27967  umgr3v3e3cycl  27969  numclwwlk1lem2foa  28139  numclwwlk5  28173  leopmul  29917  strlem3a  30035  0elsiga  31483  afsval  32052  bnj999  32340  subgrwlk  32492  cusgr3cyclex  32496  acycgrislfgr  32512  satfvsucsuc  32725  ex-sategoelel  32781  ex-sategoel  32782  conway  33377  cgr3permute3  33621  cgr3com  33627  colineardim1  33635  brofs2  33651  brifs2  33652  btwnconn1lem4  33664  btwnconn1lem5  33665  btwnconn1lem6  33666  midofsegid  33678  isbasisrelowllem1  34772  isbasisrelowllem2  34773  icoreclin  34774  ftc1anclem8  35137  sdclem2  35180  ismndo1  35311  refrelredund2  36031  lsmcv2  36325  lvolnleat  36879  paddasslem14  37129  4atexlemswapqr  37359  isltrn2N  37416  cdlemftr1  37863  cdlemg5  37901  iocinico  40162  pwinfi2  40261  relexpxpnnidm  40404  sigaras  43469  sigarms  43470  even3prm2  44237  fpprwpprb  44258  bgoldbtbndlem4  44326  bgoldbtbnd  44327  mhmismgmhm  44426  funcringcsetcALTV2lem9  44668  funcringcsetclem9ALTV  44691  fprmappr  44747  gsumlsscl  44785  ldepspr  44882  lincresunit3lem3  44883  lincresunit3lem1  44888  lincresunit3  44890  reorelicc  45124  itsclc0yqsol  45178  itsclc0  45185