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  13140  lshpsmreu  29275  exatleN  29569  2llnjaN  29731  2lplnja  29784  dalemkehl  29788  dath2  29902  pclfinN  30065  lhp2lt  30166  lhpexle3lem  30176  lhpmcvr5N  30192  lhpmcvr6N  30193  lhp2at0  30197  lhp2atnle  30198  lhp2atne  30199  lhp2at0nle  30200  lhp2at0ne  30201  4atexlemk  30212  4atexlemex6  30239  4atexlem7  30240  cdlemd2  30364  cdlemd4  30366  cdlemd7  30369  cdleme0ex2N  30389  cdleme7aa  30407  cdleme7c  30410  cdleme7d  30411  cdleme7e  30412  cdleme7ga  30413  cdleme7  30414  cdleme11c  30426  cdleme11dN  30427  cdleme11e  30428  cdleme11  30435  cdleme14  30438  cdleme15a  30439  cdleme15b  30440  cdleme15c  30441  cdleme15d  30442  cdleme15  30443  cdleme16b  30444  cdleme16c  30445  cdleme16d  30446  cdleme16e  30447  cdleme16f  30448  cdleme18d  30460  cdleme19b  30469  cdleme19d  30471  cdleme19e  30472  cdleme20d  30477  cdleme20e  30478  cdleme20f  30479  cdleme20g  30480  cdleme20h  30481  cdleme20j  30483  cdleme20k  30484  cdleme20l1  30485  cdleme20l2  30486  cdleme20l  30487  cdleme20m  30488  cdleme21c  30492  cdleme21ct  30494  cdleme21d  30495  cdleme21e  30496  cdleme22cN  30507  cdleme22f  30511  cdleme22f2  30512  cdleme22g  30513  cdleme23a  30514  cdleme23b  30515  cdleme23c  30516  cdleme25a  30518  cdleme25c  30520  cdleme25dN  30521  cdleme26ee  30525  cdleme26eALTN  30526  cdleme27a  30532  cdleme27N  30534  cdleme28a  30535  cdleme28b  30536  cdleme29ex  30539  cdlemefrs29bpre0  30561  cdlemefrs29cpre1  30563  cdlemefr29exN  30567  cdleme32fva  30602  cdleme32b  30607  cdleme32c  30608  cdleme32e  30610  cdleme35a  30613  cdleme35fnpq  30614  cdleme35b  30615  cdleme35c  30616  cdleme35d  30617  cdleme35e  30618  cdleme35f  30619  cdleme36a  30625  cdleme37m  30627  cdleme39a  30630  cdleme42e  30644  cdleme42h  30647  cdleme42i  30648  cdleme42k  30649  cdleme43bN  30655  cdleme43dN  30657  cdleme17d2  30660  cdleme48bw  30667  cdlemeg46c  30678  cdlemeg46nlpq  30682  cdlemeg46ngfr  30683  cdlemeg46frv  30690  cdlemeg46vrg  30692  cdlemeg46rgv  30693  cdlemeg46req  30694  cdlemeg46gfv  30695  cdlemf1  30726  trlord  30734  cdlemb3  30771  cdlemg7fvbwN  30772  cdlemg10a  30805  cdlemg10  30806  cdlemg12e  30812  cdlemg12f  30813  cdlemg12g  30814  cdlemg12  30815  cdlemg13a  30816  cdlemg13  30817  cdlemg17b  30827  cdlemg17g  30832  cdlemg17h  30833  cdlemg17pq  30837  cdlemg17  30842  cdlemg19a  30848  cdlemg19  30849  cdlemg21  30851  cdlemg27a  30857  cdlemg27b  30861  cdlemg31c  30864  cdlemg33b0  30866  cdlemg33c0  30867  cdlemg33a  30871  cdlemg33c  30873  cdlemg33e  30875  cdlemg35  30878  trlcone  30893  tendococl  30937  cdlemh1  30980  cdlemh2  30981  cdlemh  30982  cdlemi  30985  cdlemk5  31001  cdlemk6  31002  cdlemki  31006  cdlemksv2  31012  cdlemk7  31013  cdlemk11  31014  cdlemk12  31015  cdlemkole  31018  cdlemk14  31019  cdlemk15  31020  cdlemk17  31023  cdlemk1u  31024  cdlemk5u  31026  cdlemk6u  31027  cdlemkj  31028  cdlemkuv2  31032  cdlemk7u  31035  cdlemk11u  31036  cdlemk12u  31037  cdlemk26-3  31071  cdlemk37  31079  cdlemk11t  31111  cdlemk47  31114  cdlemk48  31115  cdlemk50  31117  cdlemk51  31118  cdlemk52  31119  cdlemk53a  31120  cdlemk39u  31133  dihord1  31384  dihord2a  31385  dihord2b  31386  dihord11b  31388  dihord11c  31390  dihord2pre  31391  dihord2pre2  31392  dihord5apre  31428  dihmeetlem1N  31456  dihglblem2N  31460  dihglblem3N  31461  dihglbcpreN  31466  dihmeetlem3N  31471  dihjatc1  31477  dihjatc2N  31478  dihjatc3  31479  dihmeetlem15N  31487
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