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

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

Proof of Theorem simp11l
StepHypRef Expression
1 simp1l 979 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pceu  12915  lshpsmreu  29921  exatleN  30215  2llnjaN  30377  2lplnja  30430  dalemkehl  30434  dath2  30548  pclfinN  30711  lhp2lt  30812  lhpexle3lem  30822  lhpmcvr5N  30838  lhpmcvr6N  30839  lhp2at0  30843  lhp2atnle  30844  lhp2atne  30845  lhp2at0nle  30846  lhp2at0ne  30847  4atexlemk  30858  4atexlemex6  30885  4atexlem7  30886  cdlemd2  31010  cdlemd4  31012  cdlemd7  31015  cdleme0ex2N  31035  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme11c  31072  cdleme11dN  31073  cdleme11e  31074  cdleme11  31081  cdleme14  31084  cdleme15a  31085  cdleme15b  31086  cdleme15c  31087  cdleme15d  31088  cdleme15  31089  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme18d  31106  cdleme19b  31115  cdleme19d  31117  cdleme19e  31118  cdleme20d  31123  cdleme20e  31124  cdleme20f  31125  cdleme20g  31126  cdleme20h  31127  cdleme20j  31129  cdleme20k  31130  cdleme20l1  31131  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme21c  31138  cdleme21ct  31140  cdleme21d  31141  cdleme21e  31142  cdleme22cN  31153  cdleme22f  31157  cdleme22f2  31158  cdleme22g  31159  cdleme23a  31160  cdleme23b  31161  cdleme23c  31162  cdleme25a  31164  cdleme25c  31166  cdleme25dN  31167  cdleme26ee  31171  cdleme26eALTN  31172  cdleme27a  31178  cdleme27N  31180  cdleme28a  31181  cdleme28b  31182  cdleme29ex  31185  cdlemefrs29bpre0  31207  cdlemefrs29cpre1  31209  cdlemefr29exN  31213  cdleme32fva  31248  cdleme32b  31253  cdleme32c  31254  cdleme32e  31256  cdleme35a  31259  cdleme35fnpq  31260  cdleme35b  31261  cdleme35c  31262  cdleme35d  31263  cdleme35e  31264  cdleme35f  31265  cdleme36a  31271  cdleme37m  31273  cdleme39a  31276  cdleme42e  31290  cdleme42h  31293  cdleme42i  31294  cdleme42k  31295  cdleme43bN  31301  cdleme43dN  31303  cdleme17d2  31306  cdleme48bw  31313  cdlemeg46c  31324  cdlemeg46nlpq  31328  cdlemeg46ngfr  31329  cdlemeg46frv  31336  cdlemeg46vrg  31338  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemeg46gfv  31341  cdlemf1  31372  trlord  31380  cdlemb3  31417  cdlemg7fvbwN  31418  cdlemg10a  31451  cdlemg10  31452  cdlemg12e  31458  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg13a  31462  cdlemg13  31463  cdlemg17b  31473  cdlemg17g  31478  cdlemg17h  31479  cdlemg17pq  31483  cdlemg17  31488  cdlemg19a  31494  cdlemg19  31495  cdlemg21  31497  cdlemg27a  31503  cdlemg27b  31507  cdlemg31c  31510  cdlemg33b0  31512  cdlemg33c0  31513  cdlemg33a  31517  cdlemg33c  31519  cdlemg33e  31521  cdlemg35  31524  trlcone  31539  tendococl  31583  cdlemh1  31626  cdlemh2  31627  cdlemh  31628  cdlemi  31631  cdlemk5  31647  cdlemk6  31648  cdlemki  31652  cdlemksv2  31658  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemkole  31664  cdlemk14  31665  cdlemk15  31666  cdlemk17  31669  cdlemk1u  31670  cdlemk5u  31672  cdlemk6u  31673  cdlemkj  31674  cdlemkuv2  31678  cdlemk7u  31681  cdlemk11u  31682  cdlemk12u  31683  cdlemk26-3  31717  cdlemk37  31725  cdlemk11t  31757  cdlemk47  31760  cdlemk48  31761  cdlemk50  31763  cdlemk51  31764  cdlemk52  31765  cdlemk53a  31766  cdlemk39u  31779  dihord1  32030  dihord2a  32031  dihord2b  32032  dihord11b  32034  dihord11c  32036  dihord2pre  32037  dihord2pre2  32038  dihord5apre  32074  dihmeetlem1N  32102  dihglblem2N  32106  dihglblem3N  32107  dihglbcpreN  32112  dihmeetlem3N  32117  dihjatc1  32123  dihjatc2N  32124  dihjatc3  32125  dihmeetlem15N  32133
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