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

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

Proof of Theorem simplr2
StepHypRef Expression
1 simpr2 1066 . 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  5493  frfi  8152  wemappo  8401  iccsplit  12250  ccatswrd  13397  pcdvdstr  15507  vdwlem12  15623  iscatd2  16266  oppccomfpropd  16311  resssetc  16666  resscatc  16679  mod1ile  17029  mod2ile  17030  prdsmndd  17247  grprcan  17379  mulgnn0dir  17495  mulgnn0di  18155  mulgdi  18156  lmodprop2d  18849  lssintcl  18886  prdslmodd  18891  islmhm2  18960  islbs3  19077  mdetmul  20351  restopnb  20892  nrmsep  21074  iunconn  21144  ptpjopn  21328  blsscls2  22222  xrsblre  22527  icccmplem2  22539  icccvx  22662  colline  25451  tglowdim2ln  25453  f1otrg  25658  f1otrge  25659  ax5seglem5  25720  axcontlem3  25753  axcontlem4  25754  axcontlem8  25758  eengtrkg  25772  2pthon3v  26715  erclwwlkstr  26809  erclwwlksntr  26821  eucrctshift  26976  frgr3v  27010  xrofsup  29389  submomnd  29507  ogrpaddltbi  29516  erdszelem8  30909  cvmliftmolem2  30993  cvmlift2lem12  31025  btwnswapid  31787  btwnsegle  31887  broutsideof3  31896  outsidele  31902  isbasisrelowllem2  32857  cvrletrN  34061  ltltncvr  34210  atcvrj2b  34219  cvrat4  34230  2at0mat0  34312  islpln2a  34335  paddasslem11  34617  pmod1i  34635  lautcvr  34879  cdlemg4c  35401  tendoplass  35572  tendodi1  35573  tendodi2  35574  mendlmod  37265  mendassa  37266  3adantlr3  38704  ssinc  38768  ssdec  38769  ioondisj2  39143  ioondisj1  39144  stoweidlem60  39600  ply1mulgsumlem2  41479  lincresunit3lem2  41573
  Copyright terms: Public domain W3C validator