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  12915  axpasch  24641  prdnei  25676  mzpcong  27162  3atlem4  30297  llncvrlpln2  30368  2lplnja  30430  2lnat  30595  llnexchb2  30680  lhp2lt  30812  lhpmcvr5N  30838  4atexlemq  30862  4atexlemex6  30885  trlval2  30974  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme11l  31080  cdleme11  31081  cdleme14  31084  cdleme15a  31085  cdleme15b  31086  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  cdleme21d  31141  cdleme21e  31142  cdleme21h  31145  cdleme22f  31157  cdleme23a  31160  cdleme23b  31161  cdleme23c  31162  cdleme24  31163  cdleme25a  31164  cdleme25dN  31167  cdleme26ee  31171  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme27a  31178  cdlemefr29bpre0N  31217  cdlemefr29clN  31218  cdlemefr32fvaN  31220  cdlemefr32fva1  31221  cdleme41sn3a  31244  cdleme35a  31259  cdleme35fnpq  31260  cdleme35b  31261  cdleme35c  31262  cdleme35d  31263  cdleme35f  31265  cdleme36m  31272  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  cdlemf  31374  cdlemg10a  31451  cdlemg10  31452  cdlemg12d  31457  cdlemg12e  31458  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg13  31463  cdlemg16ALTN  31469  cdlemg17b  31473  cdlemg17h  31479  cdlemg17pq  31483  cdlemg17iqN  31485  cdlemg17  31488  cdlemg19a  31494  cdlemg19  31495  cdlemg21  31497  cdlemg27a  31503  cdlemg27b  31507  cdlemg31c  31510  cdlemg33b0  31512  cdlemg33a  31517  cdlemg48  31548  tendocan  31635  cdlemk26-3  31717  cdlemk27-3  31718  cdlemk28-3  31719  cdlemk37  31725  cdlemky  31737  cdlemkyu  31738  cdlemk11ta  31740  cdlemkid3N  31744  cdlemk42  31752  cdlemk42yN  31755  cdlemk11t  31757  cdlemk45  31758  cdlemk46  31759  cdlemk47  31760  cdlemk51  31764  cdlemk52  31765  cdlemk53a  31766  cdleml4N  31790  dihord2pre2  32038  dihord4  32070  dihord5apre  32074  dihmeetlem1N  32102  dihmeetlem15N  32133  mapdpglem32  32517
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