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

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

Proof of Theorem simplr1
StepHypRef Expression
1 simp1 1128 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antlr 723 1 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 1081
This theorem is referenced by:  soltmin  5989  frfi  8751  wemappo  9001  iccsplit  12859  ccatswrd  14018  sqrmo  14599  pcdvdstr  16200  vdwlem12  16316  mreexexlem4d  16906  iscatd2  16940  oppccomfpropd  16985  resssetc  17340  resscatc  17353  mod1ile  17703  mod2ile  17704  prdsmndd  17932  grprcan  18075  prdsringd  19291  lmodprop2d  19625  lssintcl  19665  prdslmodd  19670  islmhm2  19739  islbs3  19856  ofco2  20988  mdetmul  21160  restopnb  21711  regsep2  21912  iunconn  21964  blsscls2  23041  met2ndci  23059  xrsblre  23346  legso  26312  colline  26362  tglowdim2ln  26364  cgrahl  26540  f1otrg  26584  f1otrge  26585  ax5seglem4  26645  ax5seglem5  26646  axcontlem4  26680  axcontlem8  26684  axcontlem9  26685  axcontlem10  26686  eengtrkg  26699  rusgrnumwwlks  27680  frgr3v  27981  submomnd  30638  ogrpaddltbi  30646  erdszelem8  32342  elmrsubrn  32664  nosupbnd1lem5  33109  conway  33161  btwncomim  33371  btwnswapid  33375  broutsideof3  33484  outsideoftr  33487  outsidele  33490  isbasisrelowllem1  34518  isbasisrelowllem2  34519  cvrletrN  36289  ltltncvr  36439  atcvrj2b  36448  2at0mat0  36541  paddasslem11  36846  pmod1i  36864  lautcvr  37108  tendoplass  37799  tendodi1  37800  tendodi2  37801  cdlemk34  37926  mendassa  39672  grumnud  40499  3adantlr3  41175  ssinc  41230  ssdec  41231  ioondisj2  41643  ioondisj1  41644  subsubelfzo0  43403  ply1mulgsumlem2  44369  lincresunit3lem2  44463
  Copyright terms: Public domain W3C validator