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

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

Proof of Theorem simprr3
StepHypRef Expression
1 simpr3 1004 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ch )
21adantl 466 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  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:  el2xptp0  6839  psgnunilem2  16391  srgbinom  17066  psgndiflemA  18504  haust1  19719  cnhaus  19721  isreg2  19744  llynlly  19844  restnlly  19849  llyrest  19852  llyidm  19855  nllyidm  19856  cldllycmp  19862  txlly  20003  txnlly  20004  pthaus  20005  txhaus  20014  txkgen  20019  xkohaus  20020  xkococnlem  20026  cmetcaulem  21593  itg2add  22032  ulmdvlem3  22662  ax5seglem6  24069  wwlkextfun  24561  frg2woteqm  24891  conpcon  28512  cvmlift3lem2  28597  cvmlift3lem8  28603  ifscgr  29628  broutsideof3  29710  icodiamlt  30690  mpaaeu  31034  stoweidlem35  31664  stoweidlem56  31685  stoweidlem59  31688  paddasslem10  35031  lhpexle2lem  35211  lhpexle3lem  35213
  Copyright terms: Public domain W3C validator