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 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3adantl3  1169  3adantr3  1172  disjtp2  4721  pr1eqbg  4858  preq12nebg  4864  otel3xp  5723  brcogw  5869  funtpg  6604  ftpg  7154  ovig  7554  el2xptp0  8022  fprresex  8295  wfrlem17OLD  8325  undifixp  8928  tz9.1c  9725  ackbij1lem16  10230  enqeq  10929  prlem934  11028  lt2halves  12447  nn0n0n1ge2  12539  ixxssixx  13338  ltdifltdiv  13799  hash2prd  14436  hashtpg  14446  pfxsuffeqwrdeq  14648  pfxccatpfx1  14686  pfxccatpfx2  14687  s3eq3seq  14890  sumtp  15695  dvdscmulr  16228  dvdsmulcr  16229  dvds2add  16233  dvds2sub  16234  dvdstr  16237  vdwlem12  16925  cshwsidrepswmod0  17028  cshwshashlem2  17030  initoeu2lem0  17963  estrreslem1  18088  estrreslem1OLD  18089  funcestrcsetclem9  18100  funcsetcestrclem9  18115  resmndismnd  18689  sgrp2nmndlem4  18809  dfgrp3e  18923  lmhmlem  20640  cnfldfunALT  20957  psgndiflemA  21154  matsc  21952  scmatrhmcl  22030  mdetdiaglem  22100  decpmatid  22272  decpmatmullem  22273  mp2pm2mplem4  22311  chfacfisf  22356  chfacfisfcpmat  22357  cpmidgsumm2pm  22371  cpmidpmat  22375  cpmadumatpoly  22385  2ndcctbss  22959  dvfsumrlim  25548  dvfsumrlim2  25549  ulmval  25892  relogbmul  26282  conway  27301  axcontlem2  28254  uspgr1v1eop  28537  uhgrissubgr  28563  subgrprop3  28564  0uhgrsubgr  28567  wlkelwrd  28921  uhgrwkspth  29043  usgr2wlkspth  29047  2pthon3v  29228  uhgr3cyclex  29466  umgr3v3e3cycl  29468  numclwwlk1lem2foa  29638  numclwwlk5  29672  leopmul  31418  strlem3a  31536  0elsiga  33143  afsval  33714  bnj999  34000  subgrwlk  34154  cusgr3cyclex  34158  acycgrislfgr  34174  satfvsucsuc  34387  ex-sategoelel  34443  ex-sategoel  34444  cgr3permute3  35050  cgr3com  35056  colineardim1  35064  brofs2  35080  brifs2  35081  btwnconn1lem4  35093  btwnconn1lem5  35094  btwnconn1lem6  35095  midofsegid  35107  gg-cnfldfunALT  35229  gg-cncrng  35231  isbasisrelowllem1  36284  isbasisrelowllem2  36285  icoreclin  36286  ftc1anclem8  36616  sdclem2  36658  ismndo1  36789  refrelredund2  37554  lsmcv2  37947  lvolnleat  38502  paddasslem14  38752  4atexlemswapqr  38982  isltrn2N  39039  cdlemftr1  39486  cdlemg5  39524  iocinico  42009  omge1  42095  pwinfi2  42361  relexpxpnnidm  42502  pimxrneun  44247  sigaras  45619  sigarms  45620  even3prm2  46435  fpprwpprb  46456  bgoldbtbndlem4  46524  bgoldbtbnd  46525  mhmismgmhm  46624  funcringcsetcALTV2lem9  46990  funcringcsetclem9ALTV  47013  fprmappr  47069  gsumlsscl  47107  ldepspr  47202  lincresunit3lem3  47203  lincresunit3lem1  47208  lincresunit3  47210  reorelicc  47444  itsclc0yqsol  47498  itsclc0  47505