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

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

Proof of Theorem simplr3
StepHypRef Expression
1 simp3 1133 . 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  swrdccat3  13692  modfsummods  14724  pcdvdstr  15782  vdwlem12  15898  cshwsidrepswmod0  16003  iscatd2  16543  oppccomfpropd  16588  initoeu2lem0  16864  resssetc  16943  resscatc  16956  yonedalem4c  17118  mod1ile  17306  mod2ile  17307  prdsmndd  17524  grprcan  17656  mulgnn0dir  17772  mulgdir  17774  mulgass  17780  mulgnn0di  18431  mulgdi  18432  dprd2da  18641  lmodprop2d  19127  lssintcl  19166  prdslmodd  19171  islmhm2  19240  islbs2  19356  islbs3  19357  dmatmul  20505  mdetmul  20631  restopnb  21181  iunconn  21433  1stcelcls  21466  blsscls2  22510  stdbdbl  22523  xrsblre  22815  icccmplem2  22827  itg1val2  23650  cvxcl  24910  colline  25743  tglowdim2ln  25745  f1otrg  25950  f1otrge  25951  ax5seglem4  26011  ax5seglem5  26012  axcontlem3  26045  axcontlem8  26050  axcontlem9  26051  eengtrkg  26064  frgr3v  27429  xrofsup  29842  submomnd  30019  ogrpaddltbi  30028  erdszelem8  31487  resconn  31535  cvmliftmolem2  31571  cvmlift2lem12  31603  conway  32216  broutsideof3  32539  outsideoftr  32542  outsidele  32545  ltltncvr  35212  atcvrj2b  35221  cvrat4  35232  cvrat42  35233  2at0mat0  35314  islpln2a  35337  paddasslem11  35619  pmod1i  35637  lhpm0atN  35818  lautcvr  35881  cdlemg4c  36402  tendoplass  36573  tendodi1  36574  tendodi2  36575  dgrsub2  38207  ssinc  39763  ssdec  39764  ioondisj2  40217  ioondisj1  40218  pfxccat3  41936  ply1mulgsumlem2  42685
  Copyright terms: Public domain W3C validator