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  12899  lshpsmreu  29299  exatleN  29593  2llnjaN  29755  2lplnja  29808  dalemkehl  29812  dath2  29926  pclfinN  30089  lhp2lt  30190  lhpexle3lem  30200  lhpmcvr5N  30216  lhpmcvr6N  30217  lhp2at0  30221  lhp2atnle  30222  lhp2atne  30223  lhp2at0nle  30224  lhp2at0ne  30225  4atexlemk  30236  4atexlemex6  30263  4atexlem7  30264  cdlemd2  30388  cdlemd4  30390  cdlemd7  30393  cdleme0ex2N  30413  cdleme7aa  30431  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme11c  30450  cdleme11dN  30451  cdleme11e  30452  cdleme11  30459  cdleme14  30462  cdleme15a  30463  cdleme15b  30464  cdleme15c  30465  cdleme15d  30466  cdleme15  30467  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme18d  30484  cdleme19b  30493  cdleme19d  30495  cdleme19e  30496  cdleme20d  30501  cdleme20e  30502  cdleme20f  30503  cdleme20g  30504  cdleme20h  30505  cdleme20j  30507  cdleme20k  30508  cdleme20l1  30509  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme21c  30516  cdleme21ct  30518  cdleme21d  30519  cdleme21e  30520  cdleme22cN  30531  cdleme22f  30535  cdleme22f2  30536  cdleme22g  30537  cdleme23a  30538  cdleme23b  30539  cdleme23c  30540  cdleme25a  30542  cdleme25c  30544  cdleme25dN  30545  cdleme26ee  30549  cdleme26eALTN  30550  cdleme27a  30556  cdleme27N  30558  cdleme28a  30559  cdleme28b  30560  cdleme29ex  30563  cdlemefrs29bpre0  30585  cdlemefrs29cpre1  30587  cdlemefr29exN  30591  cdleme32fva  30626  cdleme32b  30631  cdleme32c  30632  cdleme32e  30634  cdleme35a  30637  cdleme35fnpq  30638  cdleme35b  30639  cdleme35c  30640  cdleme35d  30641  cdleme35e  30642  cdleme35f  30643  cdleme36a  30649  cdleme37m  30651  cdleme39a  30654  cdleme42e  30668  cdleme42h  30671  cdleme42i  30672  cdleme42k  30673  cdleme43bN  30679  cdleme43dN  30681  cdleme17d2  30684  cdleme48bw  30691  cdlemeg46c  30702  cdlemeg46nlpq  30706  cdlemeg46ngfr  30707  cdlemeg46frv  30714  cdlemeg46vrg  30716  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemeg46gfv  30719  cdlemf1  30750  trlord  30758  cdlemb3  30795  cdlemg7fvbwN  30796  cdlemg10a  30829  cdlemg10  30830  cdlemg12e  30836  cdlemg12f  30837  cdlemg12g  30838  cdlemg12  30839  cdlemg13a  30840  cdlemg13  30841  cdlemg17b  30851  cdlemg17g  30856  cdlemg17h  30857  cdlemg17pq  30861  cdlemg17  30866  cdlemg19a  30872  cdlemg19  30873  cdlemg21  30875  cdlemg27a  30881  cdlemg27b  30885  cdlemg31c  30888  cdlemg33b0  30890  cdlemg33c0  30891  cdlemg33a  30895  cdlemg33c  30897  cdlemg33e  30899  cdlemg35  30902  trlcone  30917  tendococl  30961  cdlemh1  31004  cdlemh2  31005  cdlemh  31006  cdlemi  31009  cdlemk5  31025  cdlemk6  31026  cdlemki  31030  cdlemksv2  31036  cdlemk7  31037  cdlemk11  31038  cdlemk12  31039  cdlemkole  31042  cdlemk14  31043  cdlemk15  31044  cdlemk17  31047  cdlemk1u  31048  cdlemk5u  31050  cdlemk6u  31051  cdlemkj  31052  cdlemkuv2  31056  cdlemk7u  31059  cdlemk11u  31060  cdlemk12u  31061  cdlemk26-3  31095  cdlemk37  31103  cdlemk11t  31135  cdlemk47  31138  cdlemk48  31139  cdlemk50  31141  cdlemk51  31142  cdlemk52  31143  cdlemk53a  31144  cdlemk39u  31157  dihord1  31408  dihord2a  31409  dihord2b  31410  dihord11b  31412  dihord11c  31414  dihord2pre  31415  dihord2pre2  31416  dihord5apre  31452  dihmeetlem1N  31480  dihglblem2N  31484  dihglblem3N  31485  dihglbcpreN  31490  dihmeetlem3N  31495  dihjatc1  31501  dihjatc2N  31502  dihjatc3  31503  dihmeetlem15N  31511
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