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

Theorem simp12l 1068
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp12l  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ph )

Proof of Theorem simp12l
StepHypRef Expression
1 simp2l 981 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ackbij1lem16  7877  axcontlem4  24667  prdnei  25676  mzpcong  27162  eqlkr  29911  athgt  30267  llncvrlpln2  30368  4atlem11b  30419  2lnat  30595  cdlemblem  30604  pclfinN  30711  lhp2lt  30812  lhpmcvr5N  30838  lhpmcvr6N  30839  lhp2at0  30843  lhp2atnle  30844  lhp2at0nle  30846  4atexlemex6  30885  cdlemd2  31010  cdlemd7  31015  cdlemd8  31016  cdlemd9  31017  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme11c  31072  cdleme11dN  31073  cdleme11e  31074  cdleme11  31081  cdleme14  31084  cdleme15a  31085  cdleme15b  31086  cdleme15d  31088  cdleme15  31089  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme18d  31106  cdleme19b  31115  cdleme19e  31118  cdleme20d  31123  cdleme20g  31126  cdleme20h  31127  cdleme20i  31128  cdleme20j  31129  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme21c  31138  cdleme21ct  31140  cdleme21d  31141  cdleme21e  31142  cdleme22cN  31153  cdleme22f  31157  cdleme22f2  31158  cdleme23a  31160  cdleme23b  31161  cdleme23c  31162  cdleme25a  31164  cdleme25dN  31167  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdlemefr29bpre0N  31217  cdlemefr29clN  31218  cdlemefr32fvaN  31220  cdlemefr32fva1  31221  cdleme41sn3a  31244  cdleme32le  31258  cdleme35a  31259  cdleme35fnpq  31260  cdleme35b  31261  cdleme35c  31262  cdleme35d  31263  cdleme35e  31264  cdleme35f  31265  cdleme36a  31271  cdleme37m  31273  cdleme39n  31277  cdleme43bN  31301  cdleme43dN  31303  cdleme17d2  31306  cdlemeg46c  31324  cdlemeg46nlpq  31328  cdlemeg46ngfr  31329  cdlemeg46req  31340  cdlemeg46gfv  31341  cdleme50trn1  31360  cdleme50trn2a  31361  cdlemf1  31372  trlord  31380  cdlemb3  31417  cdlemg7fvbwN  31418  cdlemg7aN  31436  cdlemg10a  31451  cdlemg10  31452  cdlemg12d  31457  cdlemg12e  31458  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg13a  31462  cdlemg13  31463  cdlemg17b  31473  cdlemg17f  31477  cdlemg17g  31478  cdlemg17h  31479  cdlemg17pq  31483  cdlemg17  31488  cdlemg19a  31494  cdlemg19  31495  cdlemg21  31497  cdlemg27a  31503  cdlemg27b  31507  cdlemg31c  31510  cdlemg33b0  31512  cdlemg33a  31517  trlcone  31539  cdlemg44  31544  cdlemg48  31548  cdlemk37  31725  cdlemky  31737  cdlemk11ta  31740  cdleml4N  31790  dihord1  32030  dihord2pre2  32038  dihord4  32070  dihord5apre  32074  dihmeetlem1N  32102  dihglblem3N  32107  dihglbcpreN  32112  dihmeetlem3N  32117  dihmeetlem13N  32131  mapdpglem32  32517  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524
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