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  4720  pr1eqbg  4857  preq12nebg  4863  otel3xp  5721  brcogw  5867  funtpg  6601  ftpg  7151  ovig  7551  el2xptp0  8019  fprresex  8292  wfrlem17OLD  8322  undifixp  8925  tz9.1c  9722  ackbij1lem16  10227  enqeq  10926  prlem934  11025  lt2halves  12444  nn0n0n1ge2  12536  ixxssixx  13335  ltdifltdiv  13796  hash2prd  14433  hashtpg  14443  pfxsuffeqwrdeq  14645  pfxccatpfx1  14683  pfxccatpfx2  14684  s3eq3seq  14887  sumtp  15692  dvdscmulr  16225  dvdsmulcr  16226  dvds2add  16230  dvds2sub  16231  dvdstr  16234  vdwlem12  16922  cshwsidrepswmod0  17025  cshwshashlem2  17027  initoeu2lem0  17960  estrreslem1  18085  estrreslem1OLD  18086  funcestrcsetclem9  18097  funcsetcestrclem9  18112  resmndismnd  18686  sgrp2nmndlem4  18806  dfgrp3e  18920  lmhmlem  20633  cnfldfunALT  20950  psgndiflemA  21146  matsc  21944  scmatrhmcl  22022  mdetdiaglem  22092  decpmatid  22264  decpmatmullem  22265  mp2pm2mplem4  22303  chfacfisf  22348  chfacfisfcpmat  22349  cpmidgsumm2pm  22363  cpmidpmat  22367  cpmadumatpoly  22377  2ndcctbss  22951  dvfsumrlim  25540  dvfsumrlim2  25541  ulmval  25884  relogbmul  26272  conway  27290  axcontlem2  28213  uspgr1v1eop  28496  uhgrissubgr  28522  subgrprop3  28523  0uhgrsubgr  28526  wlkelwrd  28880  uhgrwkspth  29002  usgr2wlkspth  29006  2pthon3v  29187  uhgr3cyclex  29425  umgr3v3e3cycl  29427  numclwwlk1lem2foa  29597  numclwwlk5  29631  leopmul  31375  strlem3a  31493  0elsiga  33101  afsval  33672  bnj999  33958  subgrwlk  34112  cusgr3cyclex  34116  acycgrislfgr  34132  satfvsucsuc  34345  ex-sategoelel  34401  ex-sategoel  34402  cgr3permute3  35008  cgr3com  35014  colineardim1  35022  brofs2  35038  brifs2  35039  btwnconn1lem4  35051  btwnconn1lem5  35052  btwnconn1lem6  35053  midofsegid  35065  isbasisrelowllem1  36225  isbasisrelowllem2  36226  icoreclin  36227  ftc1anclem8  36557  sdclem2  36599  ismndo1  36730  refrelredund2  37495  lsmcv2  37888  lvolnleat  38443  paddasslem14  38693  4atexlemswapqr  38923  isltrn2N  38980  cdlemftr1  39427  cdlemg5  39465  iocinico  41947  omge1  42033  pwinfi2  42299  relexpxpnnidm  42440  pimxrneun  44186  sigaras  45558  sigarms  45559  even3prm2  46374  fpprwpprb  46395  bgoldbtbndlem4  46463  bgoldbtbnd  46464  mhmismgmhm  46563  funcringcsetcALTV2lem9  46896  funcringcsetclem9ALTV  46919  fprmappr  46975  gsumlsscl  47013  ldepspr  47108  lincresunit3lem3  47109  lincresunit3lem1  47114  lincresunit3  47116  reorelicc  47350  itsclc0yqsol  47404  itsclc0  47411