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

Theorem simplr3 1032
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 996 . 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 965
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 967
This theorem is referenced by:  soltmin  5232  frfi  7549  wemappo  7755  iccsplit  11410  ccatswrd  12342  pcdvdstr  13934  vdwlem12  14045  cshwsidrepswmod0  14113  iscatd2  14611  oppccomfpropd  14658  resssetc  14952  resscatc  14965  yonedalem4c  15079  mod1ile  15267  mod2ile  15268  prdsmndd  15446  grprcan  15562  mulgnn0dir  15641  mulgdir  15643  mulgass  15648  mulgnn0di  16304  mulgdi  16305  dprd2da  16529  lmodprop2d  16985  lssintcl  17022  prdslmodd  17027  islmhm2  17096  islbs2  17212  islbs3  17213  mdetmul  18404  restopnb  18754  iuncon  19007  1stcelcls  19040  blsscls2  20054  stdbdbl  20067  xrsblre  20363  icccmplem2  20375  itg1val2  21137  cvxcl  22353  colline  23020  f1otrg  23068  f1otrge  23069  ax5seglem4  23129  ax5seglem5  23130  axcontlem3  23163  axcontlem8  23168  axcontlem9  23169  eengtrkg  23182  xrofsup  26006  submomnd  26124  ogrpaddltbi  26133  erdszelem8  27038  rescon  27087  cvmliftmolem2  27123  cvmlift2lem12  27155  broutsideof3  28108  outsideoftr  28111  outsidele  28114  dgrsub2  29444  el2wlksotot  30354  dmatmul  30799  ltltncvr  32907  atcvrj2b  32916  cvrat4  32927  cvrat42  32928  2at0mat0  33009  islpln2a  33032  paddasslem11  33314  pmod1i  33332  lhpm0atN  33513  lautcvr  33576  cdlemg4c  34096  tendoplass  34267  tendodi1  34268  tendodi2  34269
  Copyright terms: Public domain W3C validator