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

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

Proof of Theorem simp13l
StepHypRef Expression
1 simp3l 983 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant1 976 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pceu  12899  axpasch  23980  prdnei  24985  mzpcong  26471  3atlem4  29048  llncvrlpln2  29119  2lplnja  29181  2lnat  29346  llnexchb2  29431  lhp2lt  29563  lhpmcvr5N  29589  4atexlemq  29613  4atexlemex6  29636  trlval2  29725  cdleme7d  29808  cdleme7e  29809  cdleme7ga  29810  cdleme7  29811  cdleme11l  29831  cdleme11  29832  cdleme14  29835  cdleme15a  29836  cdleme15b  29837  cdleme15  29840  cdleme16b  29841  cdleme16c  29842  cdleme16d  29843  cdleme18d  29857  cdleme19b  29866  cdleme19e  29869  cdleme20d  29874  cdleme20g  29877  cdleme20h  29878  cdleme20i  29879  cdleme20j  29880  cdleme20l2  29883  cdleme20l  29884  cdleme20m  29885  cdleme21d  29892  cdleme21e  29893  cdleme21h  29896  cdleme22f  29908  cdleme23a  29911  cdleme23b  29912  cdleme23c  29913  cdleme24  29914  cdleme25a  29915  cdleme25dN  29918  cdleme26ee  29922  cdleme26fALTN  29924  cdleme26f  29925  cdleme26f2ALTN  29926  cdleme26f2  29927  cdleme27a  29929  cdlemefr29bpre0N  29968  cdlemefr29clN  29969  cdlemefr32fvaN  29971  cdlemefr32fva1  29972  cdleme41sn3a  29995  cdleme35a  30010  cdleme35fnpq  30011  cdleme35b  30012  cdleme35c  30013  cdleme35d  30014  cdleme35f  30016  cdleme36m  30023  cdleme37m  30024  cdleme39n  30028  cdleme43bN  30052  cdleme43dN  30054  cdleme17d2  30057  cdlemeg46c  30075  cdlemeg46nlpq  30079  cdlemeg46ngfr  30080  cdlemeg46req  30091  cdlemeg46gfv  30092  cdleme50trn1  30111  cdleme50trn2a  30112  cdlemf1  30123  cdlemf  30125  cdlemg10a  30202  cdlemg10  30203  cdlemg12d  30208  cdlemg12e  30209  cdlemg12f  30210  cdlemg12g  30211  cdlemg12  30212  cdlemg13  30214  cdlemg16ALTN  30220  cdlemg17b  30224  cdlemg17h  30230  cdlemg17pq  30234  cdlemg17iqN  30236  cdlemg17  30239  cdlemg19a  30245  cdlemg19  30246  cdlemg21  30248  cdlemg27a  30254  cdlemg27b  30258  cdlemg31c  30261  cdlemg33b0  30263  cdlemg33a  30268  cdlemg48  30299  tendocan  30386  cdlemk26-3  30468  cdlemk27-3  30469  cdlemk28-3  30470  cdlemk37  30476  cdlemky  30488  cdlemkyu  30489  cdlemk11ta  30491  cdlemkid3N  30495  cdlemk42  30503  cdlemk42yN  30506  cdlemk11t  30508  cdlemk45  30509  cdlemk46  30510  cdlemk47  30511  cdlemk51  30515  cdlemk52  30516  cdlemk53a  30517  cdleml4N  30541  dihord2pre2  30789  dihord4  30821  dihord5apre  30825  dihmeetlem1N  30853  dihmeetlem15N  30884  mapdpglem32  31268
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