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

Theorem 3simpa 1142
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 1126 1 ((𝜑𝜓𝜒) → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  3simpbOLD  1145  3simpcOLD  1147  simp1OLD  1148  simp2OLD  1149  3adant3OLD  1153  3adantl3  1173  3adantr3  1176  disjtp2  4389  pr1eqbg  4522  preq12nebg  4530  otel3xp  5292  brcogw  5428  funtpg  6083  ftpg  6569  ovig  6933  el2xptp0  7365  wfrlem17  7588  undifixp  8102  tz9.1c  8774  ackbij1lem16  9263  enqeq  9962  prlem934  10061  lt2halves  11474  nn0n0n1ge2  11565  ixxssixx  12394  ltdifltdiv  12843  hash2prd  13459  hashtpg  13469  2swrdeqwrdeq  13662  swrd0swrd0  13672  swrdccatid  13706  s3eq3seq  13893  sumtp  14686  dvdscmulr  15219  dvdsmulcr  15220  dvds2add  15224  dvds2sub  15225  dvdstr  15227  vdwlem12  15903  cshwsidrepswmod0  16008  cshwshashlem2  16010  setsstructOLD  16106  initoeu2lem0  16870  estrreslem1  16984  funcestrcsetclem9  16996  funcsetcestrclem9  17011  sgrp2nmndlem4  17623  dfgrp3e  17723  lmhmlem  19242  psgndiflemA  20163  matsc  20474  scmatrhmcl  20552  mdetdiaglem  20622  decpmatid  20795  decpmatmullem  20796  mp2pm2mplem4  20834  chfacfisf  20879  chfacfisfcpmat  20880  cpmidgsumm2pm  20894  cpmidpmat  20898  cpmadumatpoly  20908  2ndcctbss  21479  dvfsumrlim  24014  dvfsumrlim2  24015  ulmval  24354  relogbmul  24736  axcontlem2  26066  funvtxvalOLD  26128  funiedgvalOLD  26129  uspgr1v1eop  26364  uhgrissubgr  26390  subgrprop3  26391  0uhgrsubgr  26394  wlkelwrd  26763  uhgrwkspth  26886  usgr2wlkspth  26890  2pthon3v  27090  clwwlknonex2e  27286  uhgr3cyclex  27362  umgr3v3e3cycl  27364  numclwwlk1lem2foa  27540  dlwwlknonclwlknonf1olem2OLD  27555  numclwwlk5  27587  leopmul  29333  strlem3a  29451  0elsiga  30517  afsval  31089  bnj999  31365  conway  32247  cgr3permute3  32491  cgr3com  32497  colineardim1  32505  brofs2  32521  brifs2  32522  btwnconn1lem4  32534  btwnconn1lem5  32535  btwnconn1lem6  32536  midofsegid  32548  isbasisrelowllem1  33539  isbasisrelowllem2  33540  icoreclin  33541  ftc1anclem8  33823  sdclem2  33868  ismndo1  34002  lsmcv2  34836  lvolnleat  35390  paddasslem14  35640  4atexlemswapqr  35870  isltrn2N  35927  cdlemftr1  36375  cdlemg5  36413  iocinico  38321  pwinfi2  38391  relexpxpnnidm  38519  sigaras  41559  sigarms  41560  pfxsuffeqwrdeq  41929  pfxccatpfx1  41950  pfxccatpfx2  41951  even3prm2  42151  bgoldbtbndlem4  42219  bgoldbtbnd  42220  mhmismgmhm  42329  funcringcsetcALTV2lem9  42567  funcringcsetclem9ALTV  42590  gsumlsscl  42687  ldepspr  42785  lincresunit3lem3  42786  lincresunit3lem1  42791  lincresunit3  42793
  Copyright terms: Public domain W3C validator