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

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

Proof of Theorem simp13r
StepHypRef Expression
1 simp3r 984 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ps )
213ad2ant1 976 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pceu  12915  axpasch  24641  prdnei  25676  3dimlem4  30275  3atlem4  30297  llncvrlpln2  30368  2lplnja  30430  lhpmcvr5N  30838  4atexlemswapqr  30874  4atexlemnclw  30881  trlval2  30974  cdleme21h  31145  cdleme24  31163  cdleme26ee  31171  cdleme26f  31174  cdleme26f2  31176  cdlemf1  31372  cdlemg16ALTN  31469  cdlemg17iqN  31485  cdlemg27b  31507  trlcone  31539  cdlemg48  31548  tendocan  31635  cdlemk26-3  31717  cdlemk27-3  31718  cdlemk28-3  31719  cdlemk37  31725  cdlemky  31737  cdlemk11ta  31740  cdlemkid3N  31744  cdlemk11t  31757  cdlemk46  31759  cdlemk47  31760  cdlemk51  31764  cdlemk52  31765  cdleml4N  31790  dihmeetlem1N  32102  dihmeetlem20N  32138  mapdpglem32  32517
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator