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 1087

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 1089

This theorem is referenced by:  3adantl3  1168  3adantr3  1171  disjtp2  4741  pr1eqbg  4881  preq12nebg  4887  otel3xp  5746  brcogw  5893  funtpg  6633  ftpg  7190  ovig  7596  el2xptp0  8077  fprresex  8351  wfrlem17OLD  8381  undifixp  8992  tz9.1c  9799  ackbij1lem16  10303  enqeq  11003  prlem934  11102  lt2halves  12528  nn0n0n1ge2  12620  ixxssixx  13421  ltdifltdiv  13885  hash2prd  14524  hashtpg  14534  pfxsuffeqwrdeq  14746  pfxccatpfx1  14784  pfxccatpfx2  14785  s3eq3seq  14988  sumtp  15797  dvdscmulr  16333  dvdsmulcr  16334  dvds2add  16338  dvds2sub  16339  dvdstr  16342  vdwlem12  17039  cshwsidrepswmod0  17142  cshwshashlem2  17144  initoeu2lem0  18080  estrreslem1  18205  estrreslem1OLD  18206  funcestrcsetclem9  18217  funcsetcestrclem9  18232  mhmismgmhm  18826  resmndismnd  18843  sgrp2nmndlem4  18963  dfgrp3e  19080  lmhmlem  21051  cnfldfunALT  21402  cnfldfunALTOLD  21415  psgndiflemA  21642  matsc  22477  scmatrhmcl  22555  mdetdiaglem  22625  decpmatid  22797  decpmatmullem  22798  mp2pm2mplem4  22836  chfacfisf  22881  chfacfisfcpmat  22882  cpmidgsumm2pm  22896  cpmidpmat  22900  cpmadumatpoly  22910  2ndcctbss  23484  dvfsumrlim  26092  dvfsumrlim2  26093  ulmval  26441  relogbmul  26838  conway  27862  axcontlem2  28998  uspgr1v1eop  29284  uhgrissubgr  29310  subgrprop3  29311  0uhgrsubgr  29314  wlkelwrd  29669  uhgrwkspth  29791  usgr2wlkspth  29795  2pthon3v  29976  uhgr3cyclex  30214  umgr3v3e3cycl  30216  numclwwlk1lem2foa  30386  numclwwlk5  30420  leopmul  32166  strlem3a  32284  0elsiga  34078  afsval  34648  bnj999  34934  subgrwlk  35100  cusgr3cyclex  35104  acycgrislfgr  35120  satfvsucsuc  35333  ex-sategoelel  35389  ex-sategoel  35390  cgr3permute3  36011  cgr3com  36017  colineardim1  36025  brofs2  36041  brifs2  36042  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem6  36056  midofsegid  36068  isbasisrelowllem1  37321  isbasisrelowllem2  37322  icoreclin  37323  ftc1anclem8  37660  sdclem2  37702  ismndo1  37833  refrelredund2  38592  lsmcv2  38985  lvolnleat  39540  paddasslem14  39790  4atexlemswapqr  40020  isltrn2N  40077  cdlemftr1  40524  cdlemg5  40562  iocinico  43173  omge1  43259  pwinfi2  43524  relexpxpnnidm  43665  pimxrneun  45404  sigaras  46776  sigarms  46777  even3prm2  47593  fpprwpprb  47614  bgoldbtbndlem4  47682  bgoldbtbnd  47683  predgclnbgrel  47711  grimgrtri  47798  grlimgrtri  47820  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044  fprmappr  48070  gsumlsscl  48108  ldepspr  48202  lincresunit3lem3  48203  lincresunit3lem1  48208  lincresunit3  48210  reorelicc  48444  itsclc0yqsol  48498  itsclc0  48505