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 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  1170  3adantr3  1173  disjtp2  4661  pr1eqbg  4801  preq12nebg  4807  otel3xp  5671  brcogw  5818  funtpg  6548  ftpg  7104  ovig  7507  el2xptp0  7983  fprresex  8254  undifixp  8876  tz9.1c  9645  ackbij1lem16  10150  enqeq  10851  prlem934  10950  lt2halves  12406  nn0n0n1ge2  12499  ixxssixx  13306  ltdifltdiv  13787  hash2prd  14431  hashtpg  14441  pfxsuffeqwrdeq  14654  pfxccatpfx1  14692  pfxccatpfx2  14693  s3eq3seq  14895  sumtp  15705  dvdscmulr  16247  dvdsmulcr  16248  dvds2add  16253  dvds2sub  16254  dvdstr  16257  vdwlem12  16957  cshwsidrepswmod0  17059  cshwshashlem2  17061  initoeu2lem0  17974  estrreslem1  18097  funcestrcsetclem9  18108  funcsetcestrclem9  18123  mhmismgmhm  18753  resmndismnd  18770  sgrp2nmndlem4  18893  dfgrp3e  19010  lmhmlem  21019  cnfldfunALT  21362  cnfldfunALTOLD  21375  psgndiflemA  21594  matsc  22428  scmatrhmcl  22506  mdetdiaglem  22576  decpmatid  22748  decpmatmullem  22749  mp2pm2mplem4  22787  chfacfisf  22832  chfacfisfcpmat  22833  cpmidgsumm2pm  22847  cpmidpmat  22851  cpmadumatpoly  22861  2ndcctbss  23433  dvfsumrlim  26011  dvfsumrlim2  26012  ulmval  26361  relogbmul  26757  conway  27788  axcontlem2  29051  uspgr1v1eop  29335  uhgrissubgr  29361  subgrprop3  29362  0uhgrsubgr  29365  wlkelwrd  29719  uhgrwkspth  29841  usgr2wlkspth  29845  2pthon3v  30029  uhgr3cyclex  30270  umgr3v3e3cycl  30272  numclwwlk1lem2foa  30442  numclwwlk5  30476  leopmul  32223  strlem3a  32341  0elsiga  34277  afsval  34834  bnj999  35119  axprALT2  35272  tz9.1regs  35297  subgrwlk  35333  cusgr3cyclex  35337  acycgrislfgr  35353  satfvsucsuc  35566  ex-sategoelel  35622  ex-sategoel  35623  cgr3permute3  36248  cgr3com  36254  colineardim1  36262  brofs2  36278  brifs2  36279  btwnconn1lem4  36291  btwnconn1lem5  36292  btwnconn1lem6  36293  midofsegid  36305  ttcexg  36733  isbasisrelowllem1  37688  isbasisrelowllem2  37689  icoreclin  37690  ftc1anclem8  38038  sdclem2  38080  ismndo1  38211  refrelredund2  39058  lsmcv2  39492  lvolnleat  40046  paddasslem14  40296  4atexlemswapqr  40526  isltrn2N  40583  cdlemftr1  41030  cdlemg5  41068  iocinico  43661  omge1  43746  pwinfi2  44010  relexpxpnnidm  44151  pimxrneun  45937  sigaras  47304  sigarms  47305  difltmodne  47811  even3prm2  48210  fpprwpprb  48231  bgoldbtbndlem4  48299  bgoldbtbnd  48300  predgclnbgrel  48330  uhgrimprop  48383  grimgrtri  48440  grlimgrtri  48494  funcringcsetcALTV2lem9  48789  funcringcsetclem9ALTV  48812  fprmappr  48836  gsumlsscl  48871  ldepspr  48964  lincresunit3lem3  48965  lincresunit3lem1  48970  lincresunit3  48972  reorelicc  49201  itsclc0yqsol  49255  itsclc0  49262