MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3simpa Structured version   Visualization version   GIF version

Theorem 3simpa 1171
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
StepHypRef Expression
1 id 22 . 2 ((𝜑𝜓) → (𝜑𝜓))
213adant3 1155 1 ((𝜑𝜓𝜒) → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  3simpbOLD  1174  3simpcOLD  1176  simp1OLD  1177  simp2OLD  1178  3adant3OLD  1182  3adantl3  1202  3adantr3  1205  disjtp2  4450  pr1eqbg  4584  preq12nebg  4592  otel3xp  5360  brcogw  5499  funtpg  6158  ftpg  6650  ovig  7015  el2xptp0  7447  wfrlem17  7670  undifixp  8184  tz9.1c  8856  ackbij1lem16  9345  enqeq  10044  prlem934  10143  lt2halves  11537  nn0n0n1ge2  11627  ixxssixx  12410  ltdifltdiv  12862  hash2prd  13477  hashtpg  13487  2swrdeqwrdeq  13680  swrd0swrd0  13690  swrdccatid  13724  s3eq3seq  13911  sumtp  14704  dvdscmulr  15236  dvdsmulcr  15237  dvds2add  15241  dvds2sub  15242  dvdstr  15244  vdwlem12  15916  cshwsidrepswmod0  16016  cshwshashlem2  16018  setsstructOLD  16113  initoeu2lem0  16870  estrreslem1  16984  funcestrcsetclem9  16996  funcsetcestrclem9  17011  sgrp2nmndlem4  17623  dfgrp3e  17723  lmhmlem  19239  psgndiflemA  20158  matsc  20471  scmatrhmcl  20549  mdetdiaglem  20619  decpmatid  20792  decpmatmullem  20793  mp2pm2mplem4  20831  chfacfisf  20876  chfacfisfcpmat  20877  cpmidgsumm2pm  20891  cpmidpmat  20895  cpmadumatpoly  20905  2ndcctbss  21476  dvfsumrlim  24014  dvfsumrlim2  24015  ulmval  24354  relogbmul  24735  axcontlem2  26065  funvtxvalOLD  26127  funiedgvalOLD  26128  uspgr1v1eop  26363  uhgrissubgr  26389  subgrprop3  26390  0uhgrsubgr  26393  wlkelwrd  26762  uhgrwkspth  26885  usgr2wlkspth  26889  2pthon3v  27089  clwwlknonex2e  27285  uhgr3cyclex  27361  umgr3v3e3cycl  27363  numclwwlk1lem2foa  27539  numclwwlk5  27582  leopmul  29327  strlem3a  29445  0elsiga  30508  afsval  31080  bnj999  31355  conway  32236  cgr3permute3  32480  cgr3com  32486  colineardim1  32494  brofs2  32510  brifs2  32511  btwnconn1lem4  32523  btwnconn1lem5  32524  btwnconn1lem6  32525  midofsegid  32537  isbasisrelowllem1  33521  isbasisrelowllem2  33522  icoreclin  33523  ftc1anclem8  33806  sdclem2  33851  ismndo1  33985  lsmcv2  34811  lvolnleat  35365  paddasslem14  35615  4atexlemswapqr  35845  isltrn2N  35902  cdlemftr1  36349  cdlemg5  36387  iocinico  38298  pwinfi2  38368  relexpxpnnidm  38496  sigaras  41527  sigarms  41528  pfxsuffeqwrdeq  41982  pfxccatpfx1  42003  pfxccatpfx2  42004  even3prm2  42204  bgoldbtbndlem4  42272  bgoldbtbnd  42273  mhmismgmhm  42375  funcringcsetcALTV2lem9  42613  funcringcsetclem9ALTV  42636  gsumlsscl  42733  ldepspr  42831  lincresunit3lem3  42832  lincresunit3lem1  42837  lincresunit3  42839
  Copyright terms: Public domain W3C validator