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  13149  lshpsmreu  29226  exatleN  29520  2llnjaN  29682  2lplnja  29735  dalemkehl  29739  dath2  29853  pclfinN  30016  lhp2lt  30117  lhpexle3lem  30127  lhpmcvr5N  30143  lhpmcvr6N  30144  lhp2at0  30148  lhp2atnle  30149  lhp2atne  30150  lhp2at0nle  30151  lhp2at0ne  30152  4atexlemk  30163  4atexlemex6  30190  4atexlem7  30191  cdlemd2  30315  cdlemd4  30317  cdlemd7  30320  cdleme0ex2N  30340  cdleme7aa  30358  cdleme7c  30361  cdleme7d  30362  cdleme7e  30363  cdleme7ga  30364  cdleme7  30365  cdleme11c  30377  cdleme11dN  30378  cdleme11e  30379  cdleme11  30386  cdleme14  30389  cdleme15a  30390  cdleme15b  30391  cdleme15c  30392  cdleme15d  30393  cdleme15  30394  cdleme16b  30395  cdleme16c  30396  cdleme16d  30397  cdleme16e  30398  cdleme16f  30399  cdleme18d  30411  cdleme19b  30420  cdleme19d  30422  cdleme19e  30423  cdleme20d  30428  cdleme20e  30429  cdleme20f  30430  cdleme20g  30431  cdleme20h  30432  cdleme20j  30434  cdleme20k  30435  cdleme20l1  30436  cdleme20l2  30437  cdleme20l  30438  cdleme20m  30439  cdleme21c  30443  cdleme21ct  30445  cdleme21d  30446  cdleme21e  30447  cdleme22cN  30458  cdleme22f  30462  cdleme22f2  30463  cdleme22g  30464  cdleme23a  30465  cdleme23b  30466  cdleme23c  30467  cdleme25a  30469  cdleme25c  30471  cdleme25dN  30472  cdleme26ee  30476  cdleme26eALTN  30477  cdleme27a  30483  cdleme27N  30485  cdleme28a  30486  cdleme28b  30487  cdleme29ex  30490  cdlemefrs29bpre0  30512  cdlemefrs29cpre1  30514  cdlemefr29exN  30518  cdleme32fva  30553  cdleme32b  30558  cdleme32c  30559  cdleme32e  30561  cdleme35a  30564  cdleme35fnpq  30565  cdleme35b  30566  cdleme35c  30567  cdleme35d  30568  cdleme35e  30569  cdleme35f  30570  cdleme36a  30576  cdleme37m  30578  cdleme39a  30581  cdleme42e  30595  cdleme42h  30598  cdleme42i  30599  cdleme42k  30600  cdleme43bN  30606  cdleme43dN  30608  cdleme17d2  30611  cdleme48bw  30618  cdlemeg46c  30629  cdlemeg46nlpq  30633  cdlemeg46ngfr  30634  cdlemeg46frv  30641  cdlemeg46vrg  30643  cdlemeg46rgv  30644  cdlemeg46req  30645  cdlemeg46gfv  30646  cdlemf1  30677  trlord  30685  cdlemb3  30722  cdlemg7fvbwN  30723  cdlemg10a  30756  cdlemg10  30757  cdlemg12e  30763  cdlemg12f  30764  cdlemg12g  30765  cdlemg12  30766  cdlemg13a  30767  cdlemg13  30768  cdlemg17b  30778  cdlemg17g  30783  cdlemg17h  30784  cdlemg17pq  30788  cdlemg17  30793  cdlemg19a  30799  cdlemg19  30800  cdlemg21  30802  cdlemg27a  30808  cdlemg27b  30812  cdlemg31c  30815  cdlemg33b0  30817  cdlemg33c0  30818  cdlemg33a  30822  cdlemg33c  30824  cdlemg33e  30826  cdlemg35  30829  trlcone  30844  tendococl  30888  cdlemh1  30931  cdlemh2  30932  cdlemh  30933  cdlemi  30936  cdlemk5  30952  cdlemk6  30953  cdlemki  30957  cdlemksv2  30963  cdlemk7  30964  cdlemk11  30965  cdlemk12  30966  cdlemkole  30969  cdlemk14  30970  cdlemk15  30971  cdlemk17  30974  cdlemk1u  30975  cdlemk5u  30977  cdlemk6u  30978  cdlemkj  30979  cdlemkuv2  30983  cdlemk7u  30986  cdlemk11u  30987  cdlemk12u  30988  cdlemk26-3  31022  cdlemk37  31030  cdlemk11t  31062  cdlemk47  31065  cdlemk48  31066  cdlemk50  31068  cdlemk51  31069  cdlemk52  31070  cdlemk53a  31071  cdlemk39u  31084  dihord1  31335  dihord2a  31336  dihord2b  31337  dihord11b  31339  dihord11c  31341  dihord2pre  31342  dihord2pre2  31343  dihord5apre  31379  dihmeetlem1N  31407  dihglblem2N  31411  dihglblem3N  31412  dihglbcpreN  31417  dihmeetlem3N  31422  dihjatc1  31428  dihjatc2N  31429  dihjatc3  31430  dihmeetlem15N  31438
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