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

Theorem simplr1 1212
 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 1133 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antlr 726 1 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  soltmin  5964  frfi  8754  wemappo  9004  iccsplit  12870  ccatswrd  14028  sqrmo  14610  pcdvdstr  16209  vdwlem12  16325  mreexexlem4d  16917  iscatd2  16951  oppccomfpropd  16996  resssetc  17351  resscatc  17364  mod1ile  17714  mod2ile  17715  prdsmndd  17943  grprcan  18137  prdsringd  19366  lmodprop2d  19697  lssintcl  19737  prdslmodd  19742  islmhm2  19811  islbs3  19928  ofco2  21070  mdetmul  21242  restopnb  21794  regsep2  21995  iunconn  22047  blsscls2  23125  met2ndci  23143  xrsblre  23430  legso  26407  colline  26457  tglowdim2ln  26459  cgrahl  26635  f1otrg  26679  f1otrge  26680  ax5seglem4  26740  ax5seglem5  26741  axcontlem4  26775  axcontlem8  26779  axcontlem9  26780  axcontlem10  26781  eengtrkg  26794  rusgrnumwwlks  27774  frgr3v  28074  submomnd  30780  ogrpaddltbi  30788  erdszelem8  32594  elmrsubrn  32916  nosupbnd1lem5  33361  conway  33413  btwncomim  33623  btwnswapid  33627  broutsideof3  33736  outsideoftr  33739  outsidele  33742  isbasisrelowllem1  34812  isbasisrelowllem2  34813  cvrletrN  36609  ltltncvr  36759  atcvrj2b  36768  2at0mat0  36861  paddasslem11  37166  pmod1i  37184  lautcvr  37428  tendoplass  38119  tendodi1  38120  tendodi2  38121  cdlemk34  38246  mendassa  40202  grumnud  41058  3adantlr3  41734  ssinc  41787  ssdec  41788  ioondisj2  42191  ioondisj1  42192  subsubelfzo0  43944  ply1mulgsumlem2  44855  lincresunit3lem2  44948
 Copyright terms: Public domain W3C validator