MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp11l 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  13208  lshpsmreu  29746  exatleN  30040  2llnjaN  30202  2lplnja  30255  dalemkehl  30259  dath2  30373  pclfinN  30536  lhp2lt  30637  lhpexle3lem  30647  lhpmcvr5N  30663  lhpmcvr6N  30664  lhp2at0  30668  lhp2atnle  30669  lhp2atne  30670  lhp2at0nle  30671  lhp2at0ne  30672  4atexlemk  30683  4atexlemex6  30710  4atexlem7  30711  cdlemd2  30835  cdlemd4  30837  cdlemd7  30840  cdleme0ex2N  30860  cdleme7aa  30878  cdleme7c  30881  cdleme7d  30882  cdleme7e  30883  cdleme7ga  30884  cdleme7  30885  cdleme11c  30897  cdleme11dN  30898  cdleme11e  30899  cdleme11  30906  cdleme14  30909  cdleme15a  30910  cdleme15b  30911  cdleme15c  30912  cdleme15d  30913  cdleme15  30914  cdleme16b  30915  cdleme16c  30916  cdleme16d  30917  cdleme16e  30918  cdleme16f  30919  cdleme18d  30931  cdleme19b  30940  cdleme19d  30942  cdleme19e  30943  cdleme20d  30948  cdleme20e  30949  cdleme20f  30950  cdleme20g  30951  cdleme20h  30952  cdleme20j  30954  cdleme20k  30955  cdleme20l1  30956  cdleme20l2  30957  cdleme20l  30958  cdleme20m  30959  cdleme21c  30963  cdleme21ct  30965  cdleme21d  30966  cdleme21e  30967  cdleme22cN  30978  cdleme22f  30982  cdleme22f2  30983  cdleme22g  30984  cdleme23a  30985  cdleme23b  30986  cdleme23c  30987  cdleme25a  30989  cdleme25c  30991  cdleme25dN  30992  cdleme26ee  30996  cdleme26eALTN  30997  cdleme27a  31003  cdleme27N  31005  cdleme28a  31006  cdleme28b  31007  cdleme29ex  31010  cdlemefrs29bpre0  31032  cdlemefrs29cpre1  31034  cdlemefr29exN  31038  cdleme32fva  31073  cdleme32b  31078  cdleme32c  31079  cdleme32e  31081  cdleme35a  31084  cdleme35fnpq  31085  cdleme35b  31086  cdleme35c  31087  cdleme35d  31088  cdleme35e  31089  cdleme35f  31090  cdleme36a  31096  cdleme37m  31098  cdleme39a  31101  cdleme42e  31115  cdleme42h  31118  cdleme42i  31119  cdleme42k  31120  cdleme43bN  31126  cdleme43dN  31128  cdleme17d2  31131  cdleme48bw  31138  cdlemeg46c  31149  cdlemeg46nlpq  31153  cdlemeg46ngfr  31154  cdlemeg46frv  31161  cdlemeg46vrg  31163  cdlemeg46rgv  31164  cdlemeg46req  31165  cdlemeg46gfv  31166  cdlemf1  31197  trlord  31205  cdlemb3  31242  cdlemg7fvbwN  31243  cdlemg10a  31276  cdlemg10  31277  cdlemg12e  31283  cdlemg12f  31284  cdlemg12g  31285  cdlemg12  31286  cdlemg13a  31287  cdlemg13  31288  cdlemg17b  31298  cdlemg17g  31303  cdlemg17h  31304  cdlemg17pq  31308  cdlemg17  31313  cdlemg19a  31319  cdlemg19  31320  cdlemg21  31322  cdlemg27a  31328  cdlemg27b  31332  cdlemg31c  31335  cdlemg33b0  31337  cdlemg33c0  31338  cdlemg33a  31342  cdlemg33c  31344  cdlemg33e  31346  cdlemg35  31349  trlcone  31364  tendococl  31408  cdlemh1  31451  cdlemh2  31452  cdlemh  31453  cdlemi  31456  cdlemk5  31472  cdlemk6  31473  cdlemki  31477  cdlemksv2  31483  cdlemk7  31484  cdlemk11  31485  cdlemk12  31486  cdlemkole  31489  cdlemk14  31490  cdlemk15  31491  cdlemk17  31494  cdlemk1u  31495  cdlemk5u  31497  cdlemk6u  31498  cdlemkj  31499  cdlemkuv2  31503  cdlemk7u  31506  cdlemk11u  31507  cdlemk12u  31508  cdlemk26-3  31542  cdlemk37  31550  cdlemk11t  31582  cdlemk47  31585  cdlemk48  31586  cdlemk50  31588  cdlemk51  31589  cdlemk52  31590  cdlemk53a  31591  cdlemk39u  31604  dihord1  31855  dihord2a  31856  dihord2b  31857  dihord11b  31859  dihord11c  31861  dihord2pre  31862  dihord2pre2  31863  dihord5apre  31899  dihmeetlem1N  31927  dihglblem2N  31931  dihglblem3N  31932  dihglbcpreN  31937  dihmeetlem3N  31942  dihjatc1  31948  dihjatc2N  31949  dihjatc3  31950  dihmeetlem15N  31958
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