MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplr3 Structured version   Unicode version

Theorem simplr3 1040
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simplr3  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ch )

Proof of Theorem simplr3
StepHypRef Expression
1 simpr3 1004 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ch )
21adantr 465 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch ) )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  soltmin  5412  frfi  7777  wemappo  7986  iccsplit  11665  ccatswrd  12661  pcdvdstr  14275  vdwlem12  14386  cshwsidrepswmod0  14454  iscatd2  14953  oppccomfpropd  15000  resssetc  15294  resscatc  15307  yonedalem4c  15421  mod1ile  15609  mod2ile  15610  prdsmndd  15826  grprcan  15955  mulgnn0dir  16037  mulgdir  16039  mulgass  16044  mulgnn0di  16707  mulgdi  16708  dprd2da  16963  lmodprop2d  17443  lssintcl  17481  prdslmodd  17486  islmhm2  17555  islbs2  17671  islbs3  17672  dmatmul  18868  mdetmul  18994  restopnb  19544  iuncon  19797  1stcelcls  19830  blsscls2  20875  stdbdbl  20888  xrsblre  21184  icccmplem2  21196  itg1val2  21959  cvxcl  23180  colline  23881  tglowdim2ln  23883  f1otrg  23988  f1otrge  23989  ax5seglem4  24049  ax5seglem5  24050  axcontlem3  24083  axcontlem8  24088  axcontlem9  24089  eengtrkg  24102  el2wlksotot  24696  xrofsup  27396  submomnd  27515  ogrpaddltbi  27524  erdszelem8  28458  rescon  28507  cvmliftmolem2  28543  cvmlift2lem12  28575  broutsideof3  29694  outsideoftr  29697  outsidele  29700  dgrsub2  31003  ioondisj2  31403  ioondisj1  31404  ply1mulgsumlem2  32424  ltltncvr  34575  atcvrj2b  34584  cvrat4  34595  cvrat42  34596  2at0mat0  34677  islpln2a  34700  paddasslem11  34982  pmod1i  35000  lhpm0atN  35181  lautcvr  35244  cdlemg4c  35764  tendoplass  35935  tendodi1  35936  tendodi2  35937
  Copyright terms: Public domain W3C validator