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

Theorem 3simpa 1148
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 1132 1 ((𝜑𝜓𝜒) → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 206  df-an 397  df-3an 1089
This theorem is referenced by:  3adantl3  1168  3adantr3  1171  disjtp2  4677  pr1eqbg  4814  preq12nebg  4820  otel3xp  5678  brcogw  5824  funtpg  6556  ftpg  7102  ovig  7501  el2xptp0  7968  fprresex  8241  wfrlem17OLD  8271  undifixp  8872  tz9.1c  9666  ackbij1lem16  10171  enqeq  10870  prlem934  10969  lt2halves  12388  nn0n0n1ge2  12480  ixxssixx  13278  ltdifltdiv  13739  hash2prd  14374  hashtpg  14384  pfxsuffeqwrdeq  14586  pfxccatpfx1  14624  pfxccatpfx2  14625  s3eq3seq  14828  sumtp  15634  dvdscmulr  16167  dvdsmulcr  16168  dvds2add  16172  dvds2sub  16173  dvdstr  16176  vdwlem12  16864  cshwsidrepswmod0  16967  cshwshashlem2  16969  initoeu2lem0  17899  estrreslem1  18024  estrreslem1OLD  18025  funcestrcsetclem9  18036  funcsetcestrclem9  18051  resmndismnd  18619  sgrp2nmndlem4  18738  dfgrp3e  18847  lmhmlem  20490  cnfldfunALT  20809  psgndiflemA  21005  matsc  21799  scmatrhmcl  21877  mdetdiaglem  21947  decpmatid  22119  decpmatmullem  22120  mp2pm2mplem4  22158  chfacfisf  22203  chfacfisfcpmat  22204  cpmidgsumm2pm  22218  cpmidpmat  22222  cpmadumatpoly  22232  2ndcctbss  22806  dvfsumrlim  25395  dvfsumrlim2  25396  ulmval  25739  relogbmul  26127  conway  27138  axcontlem2  27914  uspgr1v1eop  28197  uhgrissubgr  28223  subgrprop3  28224  0uhgrsubgr  28227  wlkelwrd  28581  uhgrwkspth  28703  usgr2wlkspth  28707  2pthon3v  28888  uhgr3cyclex  29126  umgr3v3e3cycl  29128  numclwwlk1lem2foa  29298  numclwwlk5  29332  leopmul  31076  strlem3a  31194  0elsiga  32713  afsval  33284  bnj999  33570  subgrwlk  33726  cusgr3cyclex  33730  acycgrislfgr  33746  satfvsucsuc  33959  ex-sategoelel  34015  ex-sategoel  34016  cgr3permute3  34632  cgr3com  34638  colineardim1  34646  brofs2  34662  brifs2  34663  btwnconn1lem4  34675  btwnconn1lem5  34676  btwnconn1lem6  34677  midofsegid  34689  isbasisrelowllem1  35826  isbasisrelowllem2  35827  icoreclin  35828  ftc1anclem8  36158  sdclem2  36201  ismndo1  36332  refrelredund2  37098  lsmcv2  37491  lvolnleat  38046  paddasslem14  38296  4atexlemswapqr  38526  isltrn2N  38583  cdlemftr1  39030  cdlemg5  39068  iocinico  41532  omge1  41617  pwinfi2  41824  relexpxpnnidm  41965  pimxrneun  43714  sigaras  45086  sigarms  45087  even3prm2  45901  fpprwpprb  45922  bgoldbtbndlem4  45990  bgoldbtbnd  45991  mhmismgmhm  46090  funcringcsetcALTV2lem9  46332  funcringcsetclem9ALTV  46355  fprmappr  46411  gsumlsscl  46449  ldepspr  46544  lincresunit3lem3  46545  lincresunit3lem1  46550  lincresunit3  46552  reorelicc  46786  itsclc0yqsol  46840  itsclc0  46847
  Copyright terms: Public domain W3C validator