Theorem 3simpa 1148

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adantl3  1169  3adantr3  1172  disjtp2  4697  pr1eqbg  4838  preq12nebg  4844  otel3xp  5705  brcogw  5853  funtpg  6596  ftpg  7151  ovig  7558  el2xptp0  8040  fprresex  8314  wfrlem17OLD  8344  undifixp  8953  tz9.1c  9749  ackbij1lem16  10253  enqeq  10953  prlem934  11052  lt2halves  12481  nn0n0n1ge2  12574  ixxssixx  13381  ltdifltdiv  13856  hash2prd  14498  hashtpg  14508  pfxsuffeqwrdeq  14721  pfxccatpfx1  14759  pfxccatpfx2  14760  s3eq3seq  14963  sumtp  15770  dvdscmulr  16309  dvdsmulcr  16310  dvds2add  16314  dvds2sub  16315  dvdstr  16318  vdwlem12  17017  cshwsidrepswmod0  17119  cshwshashlem2  17121  initoeu2lem0  18031  estrreslem1  18154  funcestrcsetclem9  18165  funcsetcestrclem9  18180  mhmismgmhm  18774  resmndismnd  18791  sgrp2nmndlem4  18911  dfgrp3e  19028  lmhmlem  20992  cnfldfunALT  21335  cnfldfunALTOLD  21348  psgndiflemA  21566  matsc  22393  scmatrhmcl  22471  mdetdiaglem  22541  decpmatid  22713  decpmatmullem  22714  mp2pm2mplem4  22752  chfacfisf  22797  chfacfisfcpmat  22798  cpmidgsumm2pm  22812  cpmidpmat  22816  cpmadumatpoly  22826  2ndcctbss  23398  dvfsumrlim  25995  dvfsumrlim2  25996  ulmval  26346  relogbmul  26744  conway  27768  axcontlem2  28949  uspgr1v1eop  29233  uhgrissubgr  29259  subgrprop3  29260  0uhgrsubgr  29263  wlkelwrd  29618  uhgrwkspth  29742  usgr2wlkspth  29746  2pthon3v  29930  uhgr3cyclex  30168  umgr3v3e3cycl  30170  numclwwlk1lem2foa  30340  numclwwlk5  30374  leopmul  32120  strlem3a  32238  0elsiga  34150  afsval  34708  bnj999  34994  subgrwlk  35159  cusgr3cyclex  35163  acycgrislfgr  35179  satfvsucsuc  35392  ex-sategoelel  35448  ex-sategoel  35449  cgr3permute3  36070  cgr3com  36076  colineardim1  36084  brofs2  36100  brifs2  36101  btwnconn1lem4  36113  btwnconn1lem5  36114  btwnconn1lem6  36115  midofsegid  36127  isbasisrelowllem1  37378  isbasisrelowllem2  37379  icoreclin  37380  ftc1anclem8  37729  sdclem2  37771  ismndo1  37902  refrelredund2  38659  lsmcv2  39052  lvolnleat  39607  paddasslem14  39857  4atexlemswapqr  40087  isltrn2N  40144  cdlemftr1  40591  cdlemg5  40629  iocinico  43203  omge1  43288  pwinfi2  43553  relexpxpnnidm  43694  pimxrneun  45482  sigaras  46851  sigarms  46852  difltmodne  47338  even3prm2  47700  fpprwpprb  47721  bgoldbtbndlem4  47789  bgoldbtbnd  47790  predgclnbgrel  47819  uhgrimprop  47872  grimgrtri  47928  grlimgrtri  47975  funcringcsetcALTV2lem9  48240  funcringcsetclem9ALTV  48263  fprmappr  48287  gsumlsscl  48322  ldepspr  48416  lincresunit3lem3  48417  lincresunit3lem1  48422  lincresunit3  48424  reorelicc  48657  itsclc0yqsol  48711  itsclc0  48718