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

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

Proof of Theorem simprr1
StepHypRef Expression
1 simpr1 963 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )
)  ->  ph )
21adantl 453 1  |-  ( ( ta  /\  ( th 
/\  ( ph  /\  ps  /\  ch ) ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  sqrmo  12049  haust1  17408  cnhaus  17410  isreg2  17433  llynlly  17532  restnlly  17537  llyrest  17540  llyidm  17543  nllyidm  17544  cldllycmp  17550  txlly  17660  txnlly  17661  pthaus  17662  txhaus  17671  txkgen  17676  xkohaus  17677  xkococnlem  17683  hauspwpwf1  18011  itg2add  19643  ulmdvlem3  20310  conpcon  24914  cvmliftmolem2  24961  cvmlift2lem10  24991  cvmlift3lem2  24999  cvmlift3lem8  25005  ax5seglem6  25865  broutsideof3  26052  icodiamlt  26874  mpaaeu  27323  psgnunilem2  27386  stoweidlem35  27751  stoweidlem56  27772  stoweidlem59  27775  cshwssizelem2  28244  frg2woteqm  28385  paddasslem10  30563  lhpexle2lem  30743  lhpexle3lem  30745  cdlemj3  31557  cdlemkid4  31668
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