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

Theorem simp13l 1145
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 1058 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant1 1051 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  pceu  14875  axpasch  25050  3atlem4  33122  llncvrlpln2  33193  2lplnja  33255  2lnat  33420  llnexchb2  33505  lhp2lt  33637  lhpmcvr5N  33663  4atexlemq  33687  4atexlemex6  33710  trlval2  33800  cdleme7d  33883  cdleme7e  33884  cdleme7ga  33885  cdleme7  33886  cdleme11l  33906  cdleme11  33907  cdleme14  33910  cdleme15a  33911  cdleme15b  33912  cdleme15  33915  cdleme16b  33916  cdleme16c  33917  cdleme16d  33918  cdleme18d  33932  cdleme19b  33942  cdleme19e  33945  cdleme20d  33950  cdleme20g  33953  cdleme20h  33954  cdleme20i  33955  cdleme20j  33956  cdleme20l2  33959  cdleme20l  33960  cdleme20m  33961  cdleme21d  33968  cdleme21e  33969  cdleme21h  33972  cdleme22f  33984  cdleme23a  33987  cdleme23b  33988  cdleme23c  33989  cdleme24  33990  cdleme25a  33991  cdleme25dN  33994  cdleme26ee  33998  cdleme26fALTN  34000  cdleme26f  34001  cdleme26f2ALTN  34002  cdleme26f2  34003  cdleme27a  34005  cdlemefr29bpre0N  34044  cdlemefr29clN  34045  cdlemefr32fvaN  34047  cdlemefr32fva1  34048  cdleme41sn3a  34071  cdleme35a  34086  cdleme35fnpq  34087  cdleme35b  34088  cdleme35c  34089  cdleme35d  34090  cdleme35f  34092  cdleme36m  34099  cdleme37m  34100  cdleme39n  34104  cdleme43bN  34128  cdleme43dN  34130  cdleme17d2  34133  cdlemeg46c  34151  cdlemeg46nlpq  34155  cdlemeg46ngfr  34156  cdlemeg46req  34167  cdlemeg46gfv  34168  cdleme50trn1  34187  cdleme50trn2a  34188  cdlemf1  34199  cdlemf  34201  cdlemg10a  34278  cdlemg10  34279  cdlemg12d  34284  cdlemg12e  34285  cdlemg12f  34286  cdlemg12g  34287  cdlemg12  34288  cdlemg13  34290  cdlemg16ALTN  34296  cdlemg17b  34300  cdlemg17h  34306  cdlemg17pq  34310  cdlemg17iqN  34312  cdlemg17  34315  cdlemg19a  34321  cdlemg19  34322  cdlemg21  34324  cdlemg27a  34330  cdlemg27b  34334  cdlemg31c  34337  cdlemg33b0  34339  cdlemg33a  34344  cdlemg48  34375  tendocan  34462  cdlemk26-3  34544  cdlemk27-3  34545  cdlemk28-3  34546  cdlemk37  34552  cdlemky  34564  cdlemkyu  34565  cdlemk11ta  34567  cdlemkid3N  34571  cdlemk42  34579  cdlemk42yN  34582  cdlemk11t  34584  cdlemk45  34585  cdlemk46  34586  cdlemk47  34587  cdlemk51  34591  cdlemk52  34592  cdlemk53a  34593  cdleml4N  34617  dihord2pre2  34865  dihord4  34897  dihord5apre  34901  dihmeetlem1N  34929  dihmeetlem15N  34960  mapdpglem32  35344  mzpcong  35893  mullimc  37793  mullimcf  37800  addlimc  37826
  Copyright terms: Public domain W3C validator