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  4676  pr1eqbg  4817  preq12nebg  4823  otel3xp  5677  brcogw  5822  funtpg  6555  ftpg  7110  ovig  7515  el2xptp0  7994  fprresex  8266  undifixp  8884  tz9.1c  9659  ackbij1lem16  10163  enqeq  10863  prlem934  10962  lt2halves  12393  nn0n0n1ge2  12486  ixxssixx  13296  ltdifltdiv  13772  hash2prd  14416  hashtpg  14426  pfxsuffeqwrdeq  14639  pfxccatpfx1  14677  pfxccatpfx2  14678  s3eq3seq  14881  sumtp  15691  dvdscmulr  16230  dvdsmulcr  16231  dvds2add  16236  dvds2sub  16237  dvdstr  16240  vdwlem12  16939  cshwsidrepswmod0  17041  cshwshashlem2  17043  initoeu2lem0  17955  estrreslem1  18078  funcestrcsetclem9  18089  funcsetcestrclem9  18104  mhmismgmhm  18700  resmndismnd  18717  sgrp2nmndlem4  18837  dfgrp3e  18954  lmhmlem  20968  cnfldfunALT  21311  cnfldfunALTOLD  21324  psgndiflemA  21543  matsc  22370  scmatrhmcl  22448  mdetdiaglem  22518  decpmatid  22690  decpmatmullem  22691  mp2pm2mplem4  22729  chfacfisf  22774  chfacfisfcpmat  22775  cpmidgsumm2pm  22789  cpmidpmat  22793  cpmadumatpoly  22803  2ndcctbss  23375  dvfsumrlim  25971  dvfsumrlim2  25972  ulmval  26322  relogbmul  26720  conway  27745  axcontlem2  28945  uspgr1v1eop  29229  uhgrissubgr  29255  subgrprop3  29256  0uhgrsubgr  29259  wlkelwrd  29613  uhgrwkspth  29735  usgr2wlkspth  29739  2pthon3v  29923  uhgr3cyclex  30161  umgr3v3e3cycl  30163  numclwwlk1lem2foa  30333  numclwwlk5  30367  leopmul  32113  strlem3a  32231  0elsiga  34097  afsval  34655  bnj999  34941  subgrwlk  35112  cusgr3cyclex  35116  acycgrislfgr  35132  satfvsucsuc  35345  ex-sategoelel  35401  ex-sategoel  35402  cgr3permute3  36028  cgr3com  36034  colineardim1  36042  brofs2  36058  brifs2  36059  btwnconn1lem4  36071  btwnconn1lem5  36072  btwnconn1lem6  36073  midofsegid  36085  isbasisrelowllem1  37336  isbasisrelowllem2  37337  icoreclin  37338  ftc1anclem8  37687  sdclem2  37729  ismndo1  37860  refrelredund2  38620  lsmcv2  39015  lvolnleat  39570  paddasslem14  39820  4atexlemswapqr  40050  isltrn2N  40107  cdlemftr1  40554  cdlemg5  40592  iocinico  43194  omge1  43279  pwinfi2  43544  relexpxpnnidm  43685  pimxrneun  45477  sigaras  46846  sigarms  46847  difltmodne  47336  even3prm2  47713  fpprwpprb  47734  bgoldbtbndlem4  47802  bgoldbtbnd  47803  predgclnbgrel  47832  uhgrimprop  47885  grimgrtri  47941  grlimgrtri  47988  funcringcsetcALTV2lem9  48279  funcringcsetclem9ALTV  48302  fprmappr  48326  gsumlsscl  48361  ldepspr  48455  lincresunit3lem3  48456  lincresunit3lem1  48461  lincresunit3  48463  reorelicc  48692  itsclc0yqsol  48746  itsclc0  48753