MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp11l Structured version   Unicode version

Theorem simp11l 1069
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 982 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant1 979 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  pceu  13225  lshpsmreu  29981  exatleN  30275  2llnjaN  30437  2lplnja  30490  dalemkehl  30494  dath2  30608  pclfinN  30771  lhp2lt  30872  lhpexle3lem  30882  lhpmcvr5N  30898  lhpmcvr6N  30899  lhp2at0  30903  lhp2atnle  30904  lhp2atne  30905  lhp2at0nle  30906  lhp2at0ne  30907  4atexlemk  30918  4atexlemex6  30945  4atexlem7  30946  cdlemd2  31070  cdlemd4  31072  cdlemd7  31075  cdleme0ex2N  31095  cdleme7aa  31113  cdleme7c  31116  cdleme7d  31117  cdleme7e  31118  cdleme7ga  31119  cdleme7  31120  cdleme11c  31132  cdleme11dN  31133  cdleme11e  31134  cdleme11  31141  cdleme14  31144  cdleme15a  31145  cdleme15b  31146  cdleme15c  31147  cdleme15d  31148  cdleme15  31149  cdleme16b  31150  cdleme16c  31151  cdleme16d  31152  cdleme16e  31153  cdleme16f  31154  cdleme18d  31166  cdleme19b  31175  cdleme19d  31177  cdleme19e  31178  cdleme20d  31183  cdleme20e  31184  cdleme20f  31185  cdleme20g  31186  cdleme20h  31187  cdleme20j  31189  cdleme20k  31190  cdleme20l1  31191  cdleme20l2  31192  cdleme20l  31193  cdleme20m  31194  cdleme21c  31198  cdleme21ct  31200  cdleme21d  31201  cdleme21e  31202  cdleme22cN  31213  cdleme22f  31217  cdleme22f2  31218  cdleme22g  31219  cdleme23a  31220  cdleme23b  31221  cdleme23c  31222  cdleme25a  31224  cdleme25c  31226  cdleme25dN  31227  cdleme26ee  31231  cdleme26eALTN  31232  cdleme27a  31238  cdleme27N  31240  cdleme28a  31241  cdleme28b  31242  cdleme29ex  31245  cdlemefrs29bpre0  31267  cdlemefrs29cpre1  31269  cdlemefr29exN  31273  cdleme32fva  31308  cdleme32b  31313  cdleme32c  31314  cdleme32e  31316  cdleme35a  31319  cdleme35fnpq  31320  cdleme35b  31321  cdleme35c  31322  cdleme35d  31323  cdleme35e  31324  cdleme35f  31325  cdleme36a  31331  cdleme37m  31333  cdleme39a  31336  cdleme42e  31350  cdleme42h  31353  cdleme42i  31354  cdleme42k  31355  cdleme43bN  31361  cdleme43dN  31363  cdleme17d2  31366  cdleme48bw  31373  cdlemeg46c  31384  cdlemeg46nlpq  31388  cdlemeg46ngfr  31389  cdlemeg46frv  31396  cdlemeg46vrg  31398  cdlemeg46rgv  31399  cdlemeg46req  31400  cdlemeg46gfv  31401  cdlemf1  31432  trlord  31440  cdlemb3  31477  cdlemg7fvbwN  31478  cdlemg10a  31511  cdlemg10  31512  cdlemg12e  31518  cdlemg12f  31519  cdlemg12g  31520  cdlemg12  31521  cdlemg13a  31522  cdlemg13  31523  cdlemg17b  31533  cdlemg17g  31538  cdlemg17h  31539  cdlemg17pq  31543  cdlemg17  31548  cdlemg19a  31554  cdlemg19  31555  cdlemg21  31557  cdlemg27a  31563  cdlemg27b  31567  cdlemg31c  31570  cdlemg33b0  31572  cdlemg33c0  31573  cdlemg33a  31577  cdlemg33c  31579  cdlemg33e  31581  cdlemg35  31584  trlcone  31599  tendococl  31643  cdlemh1  31686  cdlemh2  31687  cdlemh  31688  cdlemi  31691  cdlemk5  31707  cdlemk6  31708  cdlemki  31712  cdlemksv2  31718  cdlemk7  31719  cdlemk11  31720  cdlemk12  31721  cdlemkole  31724  cdlemk14  31725  cdlemk15  31726  cdlemk17  31729  cdlemk1u  31730  cdlemk5u  31732  cdlemk6u  31733  cdlemkj  31734  cdlemkuv2  31738  cdlemk7u  31741  cdlemk11u  31742  cdlemk12u  31743  cdlemk26-3  31777  cdlemk37  31785  cdlemk11t  31817  cdlemk47  31820  cdlemk48  31821  cdlemk50  31823  cdlemk51  31824  cdlemk52  31825  cdlemk53a  31826  cdlemk39u  31839  dihord1  32090  dihord2a  32091  dihord2b  32092  dihord11b  32094  dihord11c  32096  dihord2pre  32097  dihord2pre2  32098  dihord5apre  32134  dihmeetlem1N  32162  dihglblem2N  32166  dihglblem3N  32167  dihglbcpreN  32172  dihmeetlem3N  32177  dihjatc1  32183  dihjatc2N  32184  dihjatc3  32185  dihmeetlem15N  32193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator