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

Theorem simplr1 1209
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 1130 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antlr 723 1 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 1083
This theorem is referenced by:  soltmin  5993  frfi  8755  wemappo  9005  iccsplit  12864  ccatswrd  14023  sqrmo  14604  pcdvdstr  16204  vdwlem12  16320  mreexexlem4d  16910  iscatd2  16944  oppccomfpropd  16989  resssetc  17344  resscatc  17357  mod1ile  17707  mod2ile  17708  prdsmndd  17934  grprcan  18069  prdsringd  19284  lmodprop2d  19618  lssintcl  19658  prdslmodd  19663  islmhm2  19732  islbs3  19849  ofco2  20976  mdetmul  21148  restopnb  21699  regsep2  21900  iunconn  21952  blsscls2  23029  met2ndci  23047  xrsblre  23334  legso  26299  colline  26349  tglowdim2ln  26351  cgrahl  26527  f1otrg  26572  f1otrge  26573  ax5seglem4  26633  ax5seglem5  26634  axcontlem4  26668  axcontlem8  26672  axcontlem9  26673  axcontlem10  26674  eengtrkg  26687  rusgrnumwwlks  27668  frgr3v  27969  submomnd  30626  ogrpaddltbi  30634  erdszelem8  32330  elmrsubrn  32652  nosupbnd1lem5  33097  conway  33149  btwncomim  33359  btwnswapid  33363  broutsideof3  33472  outsideoftr  33475  outsidele  33478  isbasisrelowllem1  34506  isbasisrelowllem2  34507  cvrletrN  36277  ltltncvr  36427  atcvrj2b  36436  2at0mat0  36529  paddasslem11  36834  pmod1i  36852  lautcvr  37096  tendoplass  37787  tendodi1  37788  tendodi2  37789  cdlemk34  37914  mendassa  39656  grumnud  40484  3adantlr3  41160  ssinc  41215  ssdec  41216  ioondisj2  41629  ioondisj1  41630  subsubelfzo0  43389  ply1mulgsumlem2  44270  lincresunit3lem2  44364
  Copyright terms: Public domain W3C validator