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  13175  lshpsmreu  29592  exatleN  29886  2llnjaN  30048  2lplnja  30101  dalemkehl  30105  dath2  30219  pclfinN  30382  lhp2lt  30483  lhpexle3lem  30493  lhpmcvr5N  30509  lhpmcvr6N  30510  lhp2at0  30514  lhp2atnle  30515  lhp2atne  30516  lhp2at0nle  30517  lhp2at0ne  30518  4atexlemk  30529  4atexlemex6  30556  4atexlem7  30557  cdlemd2  30681  cdlemd4  30683  cdlemd7  30686  cdleme0ex2N  30706  cdleme7aa  30724  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme11c  30743  cdleme11dN  30744  cdleme11e  30745  cdleme11  30752  cdleme14  30755  cdleme15a  30756  cdleme15b  30757  cdleme15c  30758  cdleme15d  30759  cdleme15  30760  cdleme16b  30761  cdleme16c  30762  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme18d  30777  cdleme19b  30786  cdleme19d  30788  cdleme19e  30789  cdleme20d  30794  cdleme20e  30795  cdleme20f  30796  cdleme20g  30797  cdleme20h  30798  cdleme20j  30800  cdleme20k  30801  cdleme20l1  30802  cdleme20l2  30803  cdleme20l  30804  cdleme20m  30805  cdleme21c  30809  cdleme21ct  30811  cdleme21d  30812  cdleme21e  30813  cdleme22cN  30824  cdleme22f  30828  cdleme22f2  30829  cdleme22g  30830  cdleme23a  30831  cdleme23b  30832  cdleme23c  30833  cdleme25a  30835  cdleme25c  30837  cdleme25dN  30838  cdleme26ee  30842  cdleme26eALTN  30843  cdleme27a  30849  cdleme27N  30851  cdleme28a  30852  cdleme28b  30853  cdleme29ex  30856  cdlemefrs29bpre0  30878  cdlemefrs29cpre1  30880  cdlemefr29exN  30884  cdleme32fva  30919  cdleme32b  30924  cdleme32c  30925  cdleme32e  30927  cdleme35a  30930  cdleme35fnpq  30931  cdleme35b  30932  cdleme35c  30933  cdleme35d  30934  cdleme35e  30935  cdleme35f  30936  cdleme36a  30942  cdleme37m  30944  cdleme39a  30947  cdleme42e  30961  cdleme42h  30964  cdleme42i  30965  cdleme42k  30966  cdleme43bN  30972  cdleme43dN  30974  cdleme17d2  30977  cdleme48bw  30984  cdlemeg46c  30995  cdlemeg46nlpq  30999  cdlemeg46ngfr  31000  cdlemeg46frv  31007  cdlemeg46vrg  31009  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemeg46gfv  31012  cdlemf1  31043  trlord  31051  cdlemb3  31088  cdlemg7fvbwN  31089  cdlemg10a  31122  cdlemg10  31123  cdlemg12e  31129  cdlemg12f  31130  cdlemg12g  31131  cdlemg12  31132  cdlemg13a  31133  cdlemg13  31134  cdlemg17b  31144  cdlemg17g  31149  cdlemg17h  31150  cdlemg17pq  31154  cdlemg17  31159  cdlemg19a  31165  cdlemg19  31166  cdlemg21  31168  cdlemg27a  31174  cdlemg27b  31178  cdlemg31c  31181  cdlemg33b0  31183  cdlemg33c0  31184  cdlemg33a  31188  cdlemg33c  31190  cdlemg33e  31192  cdlemg35  31195  trlcone  31210  tendococl  31254  cdlemh1  31297  cdlemh2  31298  cdlemh  31299  cdlemi  31302  cdlemk5  31318  cdlemk6  31319  cdlemki  31323  cdlemksv2  31329  cdlemk7  31330  cdlemk11  31331  cdlemk12  31332  cdlemkole  31335  cdlemk14  31336  cdlemk15  31337  cdlemk17  31340  cdlemk1u  31341  cdlemk5u  31343  cdlemk6u  31344  cdlemkj  31345  cdlemkuv2  31349  cdlemk7u  31352  cdlemk11u  31353  cdlemk12u  31354  cdlemk26-3  31388  cdlemk37  31396  cdlemk11t  31428  cdlemk47  31431  cdlemk48  31432  cdlemk50  31434  cdlemk51  31435  cdlemk52  31436  cdlemk53a  31437  cdlemk39u  31450  dihord1  31701  dihord2a  31702  dihord2b  31703  dihord11b  31705  dihord11c  31707  dihord2pre  31708  dihord2pre2  31709  dihord5apre  31745  dihmeetlem1N  31773  dihglblem2N  31777  dihglblem3N  31778  dihglbcpreN  31783  dihmeetlem3N  31788  dihjatc1  31794  dihjatc2N  31795  dihjatc3  31796  dihmeetlem15N  31804
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