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

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

Proof of Theorem simp11r
StepHypRef Expression
1 simp1r 1055 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant1 1051 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  pceu  14875  maduf  19743  nllyrest  20578  exatleN  33040  2llnjaN  33202  2lplnja  33255  dalemceb  33274  pclfinN  33536  lhpexle3lem  33647  lhpmcvr5N  33663  lhpmcvr6N  33664  lhp2at0  33668  4atexlemw  33684  cdlemd2  33836  cdlemd4  33838  cdleme7aa  33879  cdleme7c  33882  cdleme7d  33883  cdleme7e  33884  cdleme7ga  33885  cdleme7  33886  cdleme15a  33911  cdleme15b  33912  cdleme15d  33914  cdleme15  33915  cdleme16b  33916  cdleme16c  33917  cdleme16d  33918  cdleme16e  33919  cdleme16f  33920  cdleme18d  33932  cdleme19b  33942  cdleme19d  33944  cdleme19e  33945  cdleme20d  33950  cdleme20e  33951  cdleme20f  33952  cdleme20g  33953  cdleme20h  33954  cdleme20j  33956  cdleme20k  33957  cdleme20l1  33958  cdleme20l2  33959  cdleme20l  33960  cdleme20m  33961  cdleme21c  33965  cdleme21ct  33967  cdleme22cN  33980  cdleme22f  33984  cdleme22g  33986  cdleme23a  33987  cdleme23b  33988  cdleme23c  33989  cdleme25a  33991  cdleme25c  33993  cdleme25dN  33994  cdleme26ee  33998  cdleme26eALTN  33999  cdleme27N  34007  cdleme28a  34008  cdleme28b  34009  cdleme29ex  34012  cdlemefr29exN  34040  cdleme32b  34080  cdleme32c  34081  cdleme32e  34083  cdleme35b  34088  cdleme35c  34089  cdleme35d  34090  cdleme35e  34091  cdleme35f  34092  cdleme42h  34120  cdleme42i  34121  cdleme42k  34122  cdleme48bw  34140  cdlemeg46frv  34163  cdlemeg46vrg  34165  cdlemeg46rgv  34166  cdlemeg46req  34167  cdlemf1  34199  trlord  34207  cdlemg7fvbwN  34245  cdlemg10  34279  cdlemg12e  34285  cdlemg12f  34286  cdlemg19a  34321  cdlemg31c  34337  cdlemg33c0  34340  cdlemg35  34351  tendococl  34410  cdlemh2  34454  cdlemh  34455  cdlemi  34458  cdlemk5  34474  cdlemk7  34486  cdlemk11  34487  cdlemk5u  34499  cdlemkj  34501  cdlemkuv2  34505  cdlemk7u  34508  cdlemk11u  34509  cdlemk26-3  34544  cdlemk11t  34584  cdlemk52  34592  cdlemk53a  34593  dihord1  34857  dihord2a  34858  dihord2b  34859  dihord11b  34861  dihord11c  34863  dihord2pre  34864  dihord2pre2  34865  dihord5apre  34901  dihmeetlem1N  34929  dihglblem2N  34933  dihglblem3N  34934  dihglbcpreN  34939  dihmeetlem3N  34944  dihjatc1  34950  suplesup  37649  limsupre  37818  limsupreOLD  37819  sge0xaddlem2  38390
  Copyright terms: Public domain W3C validator