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  5668  brcogw  5815  funtpg  6545  ftpg  7101  ovig  7504  el2xptp0  7980  fprresex  8251  undifixp  8873  tz9.1c  9640  ackbij1lem16  10145  enqeq  10846  prlem934  10945  lt2halves  12401  nn0n0n1ge2  12494  ixxssixx  13301  ltdifltdiv  13782  hash2prd  14426  hashtpg  14436  pfxsuffeqwrdeq  14649  pfxccatpfx1  14687  pfxccatpfx2  14688  s3eq3seq  14890  sumtp  15700  dvdscmulr  16242  dvdsmulcr  16243  dvds2add  16248  dvds2sub  16249  dvdstr  16252  vdwlem12  16952  cshwsidrepswmod0  17054  cshwshashlem2  17056  initoeu2lem0  17969  estrreslem1  18092  funcestrcsetclem9  18103  funcsetcestrclem9  18118  mhmismgmhm  18748  resmndismnd  18765  sgrp2nmndlem4  18888  dfgrp3e  19005  lmhmlem  21014  cnfldfunALT  21357  cnfldfunALTOLD  21370  psgndiflemA  21589  matsc  22424  scmatrhmcl  22502  mdetdiaglem  22572  decpmatid  22744  decpmatmullem  22745  mp2pm2mplem4  22783  chfacfisf  22828  chfacfisfcpmat  22829  cpmidgsumm2pm  22843  cpmidpmat  22847  cpmadumatpoly  22857  2ndcctbss  23429  dvfsumrlim  26010  dvfsumrlim2  26011  ulmval  26360  relogbmul  26758  conway  27790  axcontlem2  29053  uspgr1v1eop  29337  uhgrissubgr  29363  subgrprop3  29364  0uhgrsubgr  29367  wlkelwrd  29721  uhgrwkspth  29843  usgr2wlkspth  29847  2pthon3v  30031  uhgr3cyclex  30272  umgr3v3e3cycl  30274  numclwwlk1lem2foa  30444  numclwwlk5  30478  leopmul  32225  strlem3a  32343  0elsiga  34279  afsval  34836  bnj999  35121  axprALT2  35274  tz9.1regs  35299  subgrwlk  35335  cusgr3cyclex  35339  acycgrislfgr  35355  satfvsucsuc  35568  ex-sategoelel  35624  ex-sategoel  35625  cgr3permute3  36250  cgr3com  36256  colineardim1  36264  brofs2  36280  brifs2  36281  btwnconn1lem4  36293  btwnconn1lem5  36294  btwnconn1lem6  36295  midofsegid  36307  ttcexg  36735  isbasisrelowllem1  37682  isbasisrelowllem2  37683  icoreclin  37684  ftc1anclem8  38032  sdclem2  38074  ismndo1  38205  refrelredund2  39052  lsmcv2  39486  lvolnleat  40040  paddasslem14  40290  4atexlemswapqr  40520  isltrn2N  40577  cdlemftr1  41024  cdlemg5  41062  iocinico  43655  omge1  43740  pwinfi2  44004  relexpxpnnidm  44145  pimxrneun  45931  sigaras  47298  sigarms  47299  difltmodne  47793  even3prm2  48192  fpprwpprb  48213  bgoldbtbndlem4  48281  bgoldbtbnd  48282  predgclnbgrel  48312  uhgrimprop  48365  grimgrtri  48422  grlimgrtri  48476  funcringcsetcALTV2lem9  48771  funcringcsetclem9ALTV  48794  fprmappr  48818  gsumlsscl  48853  ldepspr  48946  lincresunit3lem3  48947  lincresunit3lem1  48952  lincresunit3  48954  reorelicc  49183  itsclc0yqsol  49237  itsclc0  49244