Theorem 3simpa 1146

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

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

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

This theorem is referenced by:  3adantl3  1166  3adantr3  1169  disjtp2  4721  pr1eqbg  4858  preq12nebg  4864  otel3xp  5724  brcogw  5871  funtpg  6608  ftpg  7165  ovig  7567  el2xptp0  8040  fprresex  8316  wfrlem17OLD  8346  undifixp  8953  tz9.1c  9754  ackbij1lem16  10259  enqeq  10958  prlem934  11057  lt2halves  12478  nn0n0n1ge2  12570  ixxssixx  13371  ltdifltdiv  13832  hash2prd  14469  hashtpg  14479  pfxsuffeqwrdeq  14681  pfxccatpfx1  14719  pfxccatpfx2  14720  s3eq3seq  14923  sumtp  15728  dvdscmulr  16262  dvdsmulcr  16263  dvds2add  16267  dvds2sub  16268  dvdstr  16271  vdwlem12  16961  cshwsidrepswmod0  17064  cshwshashlem2  17066  initoeu2lem0  18002  estrreslem1  18127  estrreslem1OLD  18128  funcestrcsetclem9  18139  funcsetcestrclem9  18154  mhmismgmhm  18748  resmndismnd  18760  sgrp2nmndlem4  18880  dfgrp3e  18996  lmhmlem  20914  cnfldfunALT  21294  cnfldfunALTOLD  21307  psgndiflemA  21533  matsc  22365  scmatrhmcl  22443  mdetdiaglem  22513  decpmatid  22685  decpmatmullem  22686  mp2pm2mplem4  22724  chfacfisf  22769  chfacfisfcpmat  22770  cpmidgsumm2pm  22784  cpmidpmat  22788  cpmadumatpoly  22798  2ndcctbss  23372  dvfsumrlim  25979  dvfsumrlim2  25980  ulmval  26329  relogbmul  26722  conway  27745  axcontlem2  28789  uspgr1v1eop  29075  uhgrissubgr  29101  subgrprop3  29102  0uhgrsubgr  29105  wlkelwrd  29460  uhgrwkspth  29582  usgr2wlkspth  29586  2pthon3v  29767  uhgr3cyclex  30005  umgr3v3e3cycl  30007  numclwwlk1lem2foa  30177  numclwwlk5  30211  leopmul  31957  strlem3a  32075  0elsiga  33733  afsval  34303  bnj999  34589  subgrwlk  34742  cusgr3cyclex  34746  acycgrislfgr  34762  satfvsucsuc  34975  ex-sategoelel  35031  ex-sategoel  35032  cgr3permute3  35643  cgr3com  35649  colineardim1  35657  brofs2  35673  brifs2  35674  btwnconn1lem4  35686  btwnconn1lem5  35687  btwnconn1lem6  35688  midofsegid  35700  isbasisrelowllem1  36834  isbasisrelowllem2  36835  icoreclin  36836  ftc1anclem8  37173  sdclem2  37215  ismndo1  37346  refrelredund2  38108  lsmcv2  38501  lvolnleat  39056  paddasslem14  39306  4atexlemswapqr  39536  isltrn2N  39593  cdlemftr1  40040  cdlemg5  40078  iocinico  42640  omge1  42726  pwinfi2  42992  relexpxpnnidm  43133  pimxrneun  44871  sigaras  46243  sigarms  46244  even3prm2  47059  fpprwpprb  47080  bgoldbtbndlem4  47148  bgoldbtbnd  47149  funcringcsetcALTV2lem9  47360  funcringcsetclem9ALTV  47383  fprmappr  47409  gsumlsscl  47447  ldepspr  47541  lincresunit3lem3  47542  lincresunit3lem1  47547  lincresunit3  47549  reorelicc  47783  itsclc0yqsol  47837  itsclc0  47844

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »