Theorem 3simpa 1147

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3adantl3  1167  3adantr3  1170  disjtp2  4652  pr1eqbg  4787  preq12nebg  4793  otel3xp  5633  brcogw  5777  funtpg  6489  ftpg  7028  ovig  7419  el2xptp0  7878  fprresex  8126  wfrlem17OLD  8156  undifixp  8722  tz9.1c  9488  ackbij1lem16  9991  enqeq  10690  prlem934  10789  lt2halves  12208  nn0n0n1ge2  12300  ixxssixx  13093  ltdifltdiv  13554  hash2prd  14189  hashtpg  14199  pfxsuffeqwrdeq  14411  pfxccatpfx1  14449  pfxccatpfx2  14450  s3eq3seq  14652  sumtp  15461  dvdscmulr  15994  dvdsmulcr  15995  dvds2add  15999  dvds2sub  16000  dvdstr  16003  vdwlem12  16693  cshwsidrepswmod0  16796  cshwshashlem2  16798  initoeu2lem0  17728  estrreslem1  17853  estrreslem1OLD  17854  funcestrcsetclem9  17865  funcsetcestrclem9  17880  resmndismnd  18447  sgrp2nmndlem4  18567  dfgrp3e  18675  lmhmlem  20291  cnfldfunALT  20610  psgndiflemA  20806  matsc  21599  scmatrhmcl  21677  mdetdiaglem  21747  decpmatid  21919  decpmatmullem  21920  mp2pm2mplem4  21958  chfacfisf  22003  chfacfisfcpmat  22004  cpmidgsumm2pm  22018  cpmidpmat  22022  cpmadumatpoly  22032  2ndcctbss  22606  dvfsumrlim  25195  dvfsumrlim2  25196  ulmval  25539  relogbmul  25927  axcontlem2  27333  uspgr1v1eop  27616  uhgrissubgr  27642  subgrprop3  27643  0uhgrsubgr  27646  wlkelwrd  28000  uhgrwkspth  28123  usgr2wlkspth  28127  2pthon3v  28308  uhgr3cyclex  28546  umgr3v3e3cycl  28548  numclwwlk1lem2foa  28718  numclwwlk5  28752  leopmul  30496  strlem3a  30614  0elsiga  32082  afsval  32651  bnj999  32938  subgrwlk  33094  cusgr3cyclex  33098  acycgrislfgr  33114  satfvsucsuc  33327  ex-sategoelel  33383  ex-sategoel  33384  conway  33993  cgr3permute3  34349  cgr3com  34355  colineardim1  34363  brofs2  34379  brifs2  34380  btwnconn1lem4  34392  btwnconn1lem5  34393  btwnconn1lem6  34394  midofsegid  34406  isbasisrelowllem1  35526  isbasisrelowllem2  35527  icoreclin  35528  ftc1anclem8  35857  sdclem2  35900  ismndo1  36031  refrelredund2  36749  lsmcv2  37043  lvolnleat  37597  paddasslem14  37847  4atexlemswapqr  38077  isltrn2N  38134  cdlemftr1  38581  cdlemg5  38619  iocinico  41043  pwinfi2  41169  relexpxpnnidm  41311  sigaras  44371  sigarms  44372  even3prm2  45171  fpprwpprb  45192  bgoldbtbndlem4  45260  bgoldbtbnd  45261  mhmismgmhm  45360  funcringcsetcALTV2lem9  45602  funcringcsetclem9ALTV  45625  fprmappr  45681  gsumlsscl  45719  ldepspr  45814  lincresunit3lem3  45815  lincresunit3lem1  45820  lincresunit3  45822  reorelicc  46056  itsclc0yqsol  46110  itsclc0  46117