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

Theorem simp11l 1068
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 981 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant1 978 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  pceu  13212  lshpsmreu  29844  exatleN  30138  2llnjaN  30300  2lplnja  30353  dalemkehl  30357  dath2  30471  pclfinN  30634  lhp2lt  30735  lhpexle3lem  30745  lhpmcvr5N  30761  lhpmcvr6N  30762  lhp2at0  30766  lhp2atnle  30767  lhp2atne  30768  lhp2at0nle  30769  lhp2at0ne  30770  4atexlemk  30781  4atexlemex6  30808  4atexlem7  30809  cdlemd2  30933  cdlemd4  30935  cdlemd7  30938  cdleme0ex2N  30958  cdleme7aa  30976  cdleme7c  30979  cdleme7d  30980  cdleme7e  30981  cdleme7ga  30982  cdleme7  30983  cdleme11c  30995  cdleme11dN  30996  cdleme11e  30997  cdleme11  31004  cdleme14  31007  cdleme15a  31008  cdleme15b  31009  cdleme15c  31010  cdleme15d  31011  cdleme15  31012  cdleme16b  31013  cdleme16c  31014  cdleme16d  31015  cdleme16e  31016  cdleme16f  31017  cdleme18d  31029  cdleme19b  31038  cdleme19d  31040  cdleme19e  31041  cdleme20d  31046  cdleme20e  31047  cdleme20f  31048  cdleme20g  31049  cdleme20h  31050  cdleme20j  31052  cdleme20k  31053  cdleme20l1  31054  cdleme20l2  31055  cdleme20l  31056  cdleme20m  31057  cdleme21c  31061  cdleme21ct  31063  cdleme21d  31064  cdleme21e  31065  cdleme22cN  31076  cdleme22f  31080  cdleme22f2  31081  cdleme22g  31082  cdleme23a  31083  cdleme23b  31084  cdleme23c  31085  cdleme25a  31087  cdleme25c  31089  cdleme25dN  31090  cdleme26ee  31094  cdleme26eALTN  31095  cdleme27a  31101  cdleme27N  31103  cdleme28a  31104  cdleme28b  31105  cdleme29ex  31108  cdlemefrs29bpre0  31130  cdlemefrs29cpre1  31132  cdlemefr29exN  31136  cdleme32fva  31171  cdleme32b  31176  cdleme32c  31177  cdleme32e  31179  cdleme35a  31182  cdleme35fnpq  31183  cdleme35b  31184  cdleme35c  31185  cdleme35d  31186  cdleme35e  31187  cdleme35f  31188  cdleme36a  31194  cdleme37m  31196  cdleme39a  31199  cdleme42e  31213  cdleme42h  31216  cdleme42i  31217  cdleme42k  31218  cdleme43bN  31224  cdleme43dN  31226  cdleme17d2  31229  cdleme48bw  31236  cdlemeg46c  31247  cdlemeg46nlpq  31251  cdlemeg46ngfr  31252  cdlemeg46frv  31259  cdlemeg46vrg  31261  cdlemeg46rgv  31262  cdlemeg46req  31263  cdlemeg46gfv  31264  cdlemf1  31295  trlord  31303  cdlemb3  31340  cdlemg7fvbwN  31341  cdlemg10a  31374  cdlemg10  31375  cdlemg12e  31381  cdlemg12f  31382  cdlemg12g  31383  cdlemg12  31384  cdlemg13a  31385  cdlemg13  31386  cdlemg17b  31396  cdlemg17g  31401  cdlemg17h  31402  cdlemg17pq  31406  cdlemg17  31411  cdlemg19a  31417  cdlemg19  31418  cdlemg21  31420  cdlemg27a  31426  cdlemg27b  31430  cdlemg31c  31433  cdlemg33b0  31435  cdlemg33c0  31436  cdlemg33a  31440  cdlemg33c  31442  cdlemg33e  31444  cdlemg35  31447  trlcone  31462  tendococl  31506  cdlemh1  31549  cdlemh2  31550  cdlemh  31551  cdlemi  31554  cdlemk5  31570  cdlemk6  31571  cdlemki  31575  cdlemksv2  31581  cdlemk7  31582  cdlemk11  31583  cdlemk12  31584  cdlemkole  31587  cdlemk14  31588  cdlemk15  31589  cdlemk17  31592  cdlemk1u  31593  cdlemk5u  31595  cdlemk6u  31596  cdlemkj  31597  cdlemkuv2  31601  cdlemk7u  31604  cdlemk11u  31605  cdlemk12u  31606  cdlemk26-3  31640  cdlemk37  31648  cdlemk11t  31680  cdlemk47  31683  cdlemk48  31684  cdlemk50  31686  cdlemk51  31687  cdlemk52  31688  cdlemk53a  31689  cdlemk39u  31702  dihord1  31953  dihord2a  31954  dihord2b  31955  dihord11b  31957  dihord11c  31959  dihord2pre  31960  dihord2pre2  31961  dihord5apre  31997  dihmeetlem1N  32025  dihglblem2N  32029  dihglblem3N  32030  dihglbcpreN  32035  dihmeetlem3N  32040  dihjatc1  32046  dihjatc2N  32047  dihjatc3  32048  dihmeetlem15N  32056
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