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

Theorem simprr3 1031
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 989 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ch )
21adantl 463 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  psgnunilem2  15981  psgndiflemA  17873  haust1  18798  cnhaus  18800  isreg2  18823  llynlly  18923  restnlly  18928  llyrest  18931  llyidm  18934  nllyidm  18935  cldllycmp  18941  txlly  19051  txnlly  19052  pthaus  19053  txhaus  19062  txkgen  19067  xkohaus  19068  xkococnlem  19074  cmetcaulem  20641  itg2add  21079  ulmdvlem3  21752  ax5seglem6  23003  conpcon  26972  cvmlift3lem2  27057  cvmlift3lem8  27063  ifscgr  27922  broutsideof3  28004  icodiamlt  29006  mpaaeu  29352  stoweidlem35  29676  stoweidlem56  29697  stoweidlem59  29700  el2xptp0  29973  wwlkextfun  30207  frg2woteqm  30498  paddasslem10  33046  lhpexle2lem  33226  lhpexle3lem  33228
  Copyright terms: Public domain W3C validator