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  12901  lshpsmreu  29372  exatleN  29666  2llnjaN  29828  2lplnja  29881  dalemkehl  29885  dath2  29999  pclfinN  30162  lhp2lt  30263  lhpexle3lem  30273  lhpmcvr5N  30289  lhpmcvr6N  30290  lhp2at0  30294  lhp2atnle  30295  lhp2atne  30296  lhp2at0nle  30297  lhp2at0ne  30298  4atexlemk  30309  4atexlemex6  30336  4atexlem7  30337  cdlemd2  30461  cdlemd4  30463  cdlemd7  30466  cdleme0ex2N  30486  cdleme7aa  30504  cdleme7c  30507  cdleme7d  30508  cdleme7e  30509  cdleme7ga  30510  cdleme7  30511  cdleme11c  30523  cdleme11dN  30524  cdleme11e  30525  cdleme11  30532  cdleme14  30535  cdleme15a  30536  cdleme15b  30537  cdleme15c  30538  cdleme15d  30539  cdleme15  30540  cdleme16b  30541  cdleme16c  30542  cdleme16d  30543  cdleme16e  30544  cdleme16f  30545  cdleme18d  30557  cdleme19b  30566  cdleme19d  30568  cdleme19e  30569  cdleme20d  30574  cdleme20e  30575  cdleme20f  30576  cdleme20g  30577  cdleme20h  30578  cdleme20j  30580  cdleme20k  30581  cdleme20l1  30582  cdleme20l2  30583  cdleme20l  30584  cdleme20m  30585  cdleme21c  30589  cdleme21ct  30591  cdleme21d  30592  cdleme21e  30593  cdleme22cN  30604  cdleme22f  30608  cdleme22f2  30609  cdleme22g  30610  cdleme23a  30611  cdleme23b  30612  cdleme23c  30613  cdleme25a  30615  cdleme25c  30617  cdleme25dN  30618  cdleme26ee  30622  cdleme26eALTN  30623  cdleme27a  30629  cdleme27N  30631  cdleme28a  30632  cdleme28b  30633  cdleme29ex  30636  cdlemefrs29bpre0  30658  cdlemefrs29cpre1  30660  cdlemefr29exN  30664  cdleme32fva  30699  cdleme32b  30704  cdleme32c  30705  cdleme32e  30707  cdleme35a  30710  cdleme35fnpq  30711  cdleme35b  30712  cdleme35c  30713  cdleme35d  30714  cdleme35e  30715  cdleme35f  30716  cdleme36a  30722  cdleme37m  30724  cdleme39a  30727  cdleme42e  30741  cdleme42h  30744  cdleme42i  30745  cdleme42k  30746  cdleme43bN  30752  cdleme43dN  30754  cdleme17d2  30757  cdleme48bw  30764  cdlemeg46c  30775  cdlemeg46nlpq  30779  cdlemeg46ngfr  30780  cdlemeg46frv  30787  cdlemeg46vrg  30789  cdlemeg46rgv  30790  cdlemeg46req  30791  cdlemeg46gfv  30792  cdlemf1  30823  trlord  30831  cdlemb3  30868  cdlemg7fvbwN  30869  cdlemg10a  30902  cdlemg10  30903  cdlemg12e  30909  cdlemg12f  30910  cdlemg12g  30911  cdlemg12  30912  cdlemg13a  30913  cdlemg13  30914  cdlemg17b  30924  cdlemg17g  30929  cdlemg17h  30930  cdlemg17pq  30934  cdlemg17  30939  cdlemg19a  30945  cdlemg19  30946  cdlemg21  30948  cdlemg27a  30954  cdlemg27b  30958  cdlemg31c  30961  cdlemg33b0  30963  cdlemg33c0  30964  cdlemg33a  30968  cdlemg33c  30970  cdlemg33e  30972  cdlemg35  30975  trlcone  30990  tendococl  31034  cdlemh1  31077  cdlemh2  31078  cdlemh  31079  cdlemi  31082  cdlemk5  31098  cdlemk6  31099  cdlemki  31103  cdlemksv2  31109  cdlemk7  31110  cdlemk11  31111  cdlemk12  31112  cdlemkole  31115  cdlemk14  31116  cdlemk15  31117  cdlemk17  31120  cdlemk1u  31121  cdlemk5u  31123  cdlemk6u  31124  cdlemkj  31125  cdlemkuv2  31129  cdlemk7u  31132  cdlemk11u  31133  cdlemk12u  31134  cdlemk26-3  31168  cdlemk37  31176  cdlemk11t  31208  cdlemk47  31211  cdlemk48  31212  cdlemk50  31214  cdlemk51  31215  cdlemk52  31216  cdlemk53a  31217  cdlemk39u  31230  dihord1  31481  dihord2a  31482  dihord2b  31483  dihord11b  31485  dihord11c  31487  dihord2pre  31488  dihord2pre2  31489  dihord5apre  31525  dihmeetlem1N  31553  dihglblem2N  31557  dihglblem3N  31558  dihglbcpreN  31563  dihmeetlem3N  31568  dihjatc1  31574  dihjatc2N  31575  dihjatc3  31576  dihmeetlem15N  31584
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