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

Theorem simprr3 1007
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 965 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ch )
21adantl 453 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  haust1  17416  cnhaus  17418  isreg2  17441  llynlly  17540  restnlly  17545  llyrest  17548  llyidm  17551  nllyidm  17552  cldllycmp  17558  txlly  17668  txnlly  17669  pthaus  17670  txhaus  17679  txkgen  17684  xkohaus  17685  xkococnlem  17691  cmetcaulem  19241  itg2add  19651  ulmdvlem3  20318  conpcon  24922  cvmlift3lem2  25007  cvmlift3lem8  25013  ax5seglem6  25873  ifscgr  25978  broutsideof3  26060  icodiamlt  26883  mpaaeu  27332  psgnunilem2  27395  stoweidlem35  27760  stoweidlem56  27781  stoweidlem59  27784  el2xptp0  28061  cshwssizelem2  28281  frg2woteqm  28448  paddasslem10  30626  lhpexle2lem  30806  lhpexle3lem  30808
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator