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 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  3adantl3  1162  3adantr3  1165  disjtp2  4650  pr1eqbg  4785  preq12nebg  4791  otel3xp  5597  brcogw  5737  funtpg  6405  ftpg  6913  ovig  7289  el2xptp0  7730  wfrlem17  7965  undifixp  8490  tz9.1c  9164  ackbij1lem16  9649  enqeq  10348  prlem934  10447  lt2halves  11864  nn0n0n1ge2  11954  ixxssixx  12745  ltdifltdiv  13197  hash2prd  13826  hashtpg  13836  pfxsuffeqwrdeq  14053  pfxccatpfx1  14091  pfxccatpfx2  14092  s3eq3seq  14294  sumtp  15096  dvdscmulr  15630  dvdsmulcr  15631  dvds2add  15635  dvds2sub  15636  dvdstr  15638  vdwlem12  16320  cshwsidrepswmod0  16420  cshwshashlem2  16422  initoeu2lem0  17265  estrreslem1  17379  funcestrcsetclem9  17390  funcsetcestrclem9  17405  sgrp2nmndlem4  18028  dfgrp3e  18131  lmhmlem  19723  psgndiflemA  20663  matsc  20977  scmatrhmcl  21055  mdetdiaglem  21125  decpmatid  21296  decpmatmullem  21297  mp2pm2mplem4  21335  chfacfisf  21380  chfacfisfcpmat  21381  cpmidgsumm2pm  21395  cpmidpmat  21399  cpmadumatpoly  21409  2ndcctbss  21981  dvfsumrlim  24545  dvfsumrlim2  24546  ulmval  24885  relogbmul  25270  axcontlem2  26667  uspgr1v1eop  26947  uhgrissubgr  26973  subgrprop3  26974  0uhgrsubgr  26977  wlkelwrd  27330  uhgrwkspth  27452  usgr2wlkspth  27456  2pthon3v  27638  uhgr3cyclex  27877  umgr3v3e3cycl  27879  numclwwlk1lem2foa  28049  numclwwlk5  28083  leopmul  29827  strlem3a  29945  0elsiga  31261  afsval  31830  bnj999  32117  subgrwlk  32265  cusgr3cyclex  32269  acycgrislfgr  32285  satfvsucsuc  32498  ex-sategoelel  32554  ex-sategoel  32555  conway  33150  cgr3permute3  33394  cgr3com  33400  colineardim1  33408  brofs2  33424  brifs2  33425  btwnconn1lem4  33437  btwnconn1lem5  33438  btwnconn1lem6  33439  midofsegid  33451  isbasisrelowllem1  34507  isbasisrelowllem2  34508  icoreclin  34509  ftc1anclem8  34843  sdclem2  34887  ismndo1  35021  refrelredund2  35740  lsmcv2  36034  lvolnleat  36588  paddasslem14  36838  4atexlemswapqr  37068  isltrn2N  37125  cdlemftr1  37572  cdlemg5  37610  iocinico  39685  pwinfi2  39788  relexpxpnnidm  39915  sigaras  42980  sigarms  42981  even3prm2  43718  fpprwpprb  43739  bgoldbtbndlem4  43807  bgoldbtbnd  43808  mhmismgmhm  43907  funcringcsetcALTV2lem9  44149  funcringcsetclem9ALTV  44172  gsumlsscl  44265  ldepspr  44362  lincresunit3lem3  44363  lincresunit3lem1  44368  lincresunit3  44370  reorelicc  44531  itsclc0yqsol  44585  itsclc0  44592
  Copyright terms: Public domain W3C validator