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

Theorem simplr2 1262
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 1131 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antlr 706 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:  soltmin  5671  frfi  8359  wemappo  8608  iccsplit  12505  ccatswrd  13658  pcdvdstr  15780  vdwlem12  15896  iscatd2  16542  oppccomfpropd  16587  resssetc  16942  resscatc  16955  mod1ile  17306  mod2ile  17307  prdsmndd  17524  grprcan  17656  mulgnn0dir  17772  mulgnn0di  18431  mulgdi  18432  lmodprop2d  19128  lssintcl  19170  prdslmodd  19175  islmhm2  19244  islbs3  19363  mdetmul  20640  restopnb  21193  nrmsep  21375  iunconn  21445  ptpjopn  21629  blsscls2  22522  xrsblre  22827  icccmplem2  22839  icccvx  22962  colline  25758  tglowdim2ln  25760  f1otrg  25965  f1otrge  25966  ax5seglem5  26027  axcontlem3  26060  axcontlem4  26061  axcontlem8  26065  eengtrkg  26079  2pthon3v  27083  erclwwlktr  27165  erclwwlkntr  27222  eucrctshift  27416  frgr3v  27450  frgr2wwlkeqm  27506  xrofsup  29866  submomnd  30043  ogrpaddltbi  30052  erdszelem8  31511  cvmliftmolem2  31595  cvmlift2lem12  31627  conway  32240  btwnswapid  32454  btwnsegle  32554  broutsideof3  32563  outsidele  32569  isbasisrelowllem2  33534  cvrletrN  35075  ltltncvr  35224  atcvrj2b  35233  cvrat4  35244  2at0mat0  35326  islpln2a  35349  paddasslem11  35631  pmod1i  35649  lautcvr  35893  cdlemg4c  36414  tendoplass  36585  tendodi1  36586  tendodi2  36587  mendlmod  38282  mendassa  38283  3adantlr3  39715  ssinc  39778  ssdec  39779  ioondisj2  40228  ioondisj1  40229  stoweidlem60  40787  ply1mulgsumlem2  42696  lincresunit3lem2  42790
  Copyright terms: Public domain W3C validator