Theorem 3simpa 1144

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3adantl3  1164  3adantr3  1167  disjtp2  4652  pr1eqbg  4787  preq12nebg  4793  otel3xp  5599  brcogw  5739  funtpg  6409  ftpg  6918  ovig  7296  el2xptp0  7736  wfrlem17  7971  undifixp  8498  tz9.1c  9172  ackbij1lem16  9657  enqeq  10356  prlem934  10455  lt2halves  11873  nn0n0n1ge2  11963  ixxssixx  12753  ltdifltdiv  13205  hash2prd  13834  hashtpg  13844  pfxsuffeqwrdeq  14060  pfxccatpfx1  14098  pfxccatpfx2  14099  s3eq3seq  14301  sumtp  15104  dvdscmulr  15638  dvdsmulcr  15639  dvds2add  15643  dvds2sub  15644  dvdstr  15646  vdwlem12  16328  cshwsidrepswmod0  16428  cshwshashlem2  16430  initoeu2lem0  17273  estrreslem1  17387  funcestrcsetclem9  17398  funcsetcestrclem9  17413  resmndismnd  17973  sgrp2nmndlem4  18093  dfgrp3e  18199  lmhmlem  19801  psgndiflemA  20745  matsc  21059  scmatrhmcl  21137  mdetdiaglem  21207  decpmatid  21378  decpmatmullem  21379  mp2pm2mplem4  21417  chfacfisf  21462  chfacfisfcpmat  21463  cpmidgsumm2pm  21477  cpmidpmat  21481  cpmadumatpoly  21491  2ndcctbss  22063  dvfsumrlim  24628  dvfsumrlim2  24629  ulmval  24968  relogbmul  25355  axcontlem2  26751  uspgr1v1eop  27031  uhgrissubgr  27057  subgrprop3  27058  0uhgrsubgr  27061  wlkelwrd  27414  uhgrwkspth  27536  usgr2wlkspth  27540  2pthon3v  27722  uhgr3cyclex  27961  umgr3v3e3cycl  27963  numclwwlk1lem2foa  28133  numclwwlk5  28167  leopmul  29911  strlem3a  30029  0elsiga  31373  afsval  31942  bnj999  32230  subgrwlk  32379  cusgr3cyclex  32383  acycgrislfgr  32399  satfvsucsuc  32612  ex-sategoelel  32668  ex-sategoel  32669  conway  33264  cgr3permute3  33508  cgr3com  33514  colineardim1  33522  brofs2  33538  brifs2  33539  btwnconn1lem4  33551  btwnconn1lem5  33552  btwnconn1lem6  33553  midofsegid  33565  isbasisrelowllem1  34639  isbasisrelowllem2  34640  icoreclin  34641  ftc1anclem8  34989  sdclem2  35032  ismndo1  35166  refrelredund2  35886  lsmcv2  36180  lvolnleat  36734  paddasslem14  36984  4atexlemswapqr  37214  isltrn2N  37271  cdlemftr1  37718  cdlemg5  37756  iocinico  39867  pwinfi2  39970  relexpxpnnidm  40097  sigaras  43161  sigarms  43162  even3prm2  43933  fpprwpprb  43954  bgoldbtbndlem4  44022  bgoldbtbnd  44023  mhmismgmhm  44122  funcringcsetcALTV2lem9  44364  funcringcsetclem9ALTV  44387  gsumlsscl  44480  ldepspr  44577  lincresunit3lem3  44578  lincresunit3lem1  44583  lincresunit3  44585  reorelicc  44746  itsclc0yqsol  44800  itsclc0  44807