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

Theorem simplr2 1263
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simplr2 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜓)

Proof of Theorem simplr2
StepHypRef Expression
1 simp2 1132 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antlr 765 1 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  soltmin  5690  frfi  8370  wemappo  8619  iccsplit  12498  ccatswrd  13656  pcdvdstr  15782  vdwlem12  15898  iscatd2  16543  oppccomfpropd  16588  resssetc  16943  resscatc  16956  mod1ile  17306  mod2ile  17307  prdsmndd  17524  grprcan  17656  mulgnn0dir  17772  mulgnn0di  18431  mulgdi  18432  lmodprop2d  19127  lssintcl  19166  prdslmodd  19171  islmhm2  19240  islbs3  19357  mdetmul  20631  restopnb  21181  nrmsep  21363  iunconn  21433  ptpjopn  21617  blsscls2  22510  xrsblre  22815  icccmplem2  22827  icccvx  22950  colline  25743  tglowdim2ln  25745  f1otrg  25950  f1otrge  25951  ax5seglem5  26012  axcontlem3  26045  axcontlem4  26046  axcontlem8  26050  eengtrkg  26064  2pthon3v  27063  erclwwlktr  27145  erclwwlkntr  27202  eucrctshift  27395  frgr3v  27429  frgr2wwlkeqm  27485  xrofsup  29842  submomnd  30019  ogrpaddltbi  30028  erdszelem8  31487  cvmliftmolem2  31571  cvmlift2lem12  31603  conway  32216  btwnswapid  32430  btwnsegle  32530  broutsideof3  32539  outsidele  32545  isbasisrelowllem2  33515  cvrletrN  35063  ltltncvr  35212  atcvrj2b  35221  cvrat4  35232  2at0mat0  35314  islpln2a  35337  paddasslem11  35619  pmod1i  35637  lautcvr  35881  cdlemg4c  36402  tendoplass  36573  tendodi1  36574  tendodi2  36575  mendlmod  38265  mendassa  38266  3adantlr3  39699  ssinc  39763  ssdec  39764  ioondisj2  40217  ioondisj1  40218  stoweidlem60  40780  ply1mulgsumlem2  42685  lincresunit3lem2  42779
  Copyright terms: Public domain W3C validator