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

Theorem simplr1 1101
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simplr1 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜑)

Proof of Theorem simplr1
StepHypRef Expression
1 simpr1 1065 . 2 ((𝜃 ∧ (𝜑𝜓𝜒)) → 𝜑)
21adantr 481 1 (((𝜃 ∧ (𝜑𝜓𝜒)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  soltmin  5495  frfi  8150  wemappo  8399  iccsplit  12244  ccatswrd  13389  sqrmo  13921  pcdvdstr  15499  vdwlem12  15615  mreexexlem4d  16223  iscatd2  16258  oppccomfpropd  16303  resssetc  16658  resscatc  16671  mod1ile  17021  mod2ile  17022  prdsmndd  17239  grprcan  17371  prdsringd  18528  lmodprop2d  18841  lssintcl  18878  prdslmodd  18883  islmhm2  18952  islbs3  19069  ofco2  20171  mdetmul  20343  restopnb  20884  regsep2  21085  iunconn  21136  blsscls2  22214  met2ndci  22232  xrsblre  22517  legso  25389  colline  25439  tglowdim2ln  25441  cgrahl  25613  f1otrg  25646  f1otrge  25647  ax5seglem4  25707  ax5seglem5  25708  axcontlem4  25742  axcontlem8  25746  axcontlem9  25747  axcontlem10  25748  eengtrkg  25760  rusgrnumwwlks  26730  frgr3v  26997  submomnd  29487  ogrpaddltbi  29496  erdszelem8  30880  btwncomim  31754  btwnswapid  31758  broutsideof3  31867  outsideoftr  31870  outsidele  31873  isbasisrelowllem1  32827  isbasisrelowllem2  32828  cvrletrN  34026  ltltncvr  34175  atcvrj2b  34184  2at0mat0  34277  paddasslem11  34582  pmod1i  34600  lautcvr  34844  tendoplass  35537  tendodi1  35538  tendodi2  35539  cdlemk34  35664  mendassa  37231  3adantlr3  38669  ssinc  38735  ssdec  38736  ioondisj2  39112  ioondisj1  39113  subsubelfzo0  40621  ply1mulgsumlem2  41437  lincresunit3lem2  41531
  Copyright terms: Public domain W3C validator