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

Theorem simprr3 1038
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 996 . 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 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:  psgnunilem2  16022  srgbinom  16665  psgndiflemA  18053  haust1  18978  cnhaus  18980  isreg2  19003  llynlly  19103  restnlly  19108  llyrest  19111  llyidm  19114  nllyidm  19115  cldllycmp  19121  txlly  19231  txnlly  19232  pthaus  19233  txhaus  19242  txkgen  19247  xkohaus  19248  xkococnlem  19254  cmetcaulem  20821  itg2add  21259  ulmdvlem3  21889  ax5seglem6  23202  conpcon  27146  cvmlift3lem2  27231  cvmlift3lem8  27237  ifscgr  28097  broutsideof3  28179  icodiamlt  29187  mpaaeu  29533  stoweidlem35  29856  stoweidlem56  29877  stoweidlem59  29880  el2xptp0  30153  wwlkextfun  30387  frg2woteqm  30678  paddasslem10  33569  lhpexle2lem  33749  lhpexle3lem  33751
  Copyright terms: Public domain W3C validator