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

Theorem simp13l 1072
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 985 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant1 978 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  pceu  13220  axpasch  25880  mzpcong  27037  3atlem4  30283  llncvrlpln2  30354  2lplnja  30416  2lnat  30581  llnexchb2  30666  lhp2lt  30798  lhpmcvr5N  30824  4atexlemq  30848  4atexlemex6  30871  trlval2  30960  cdleme7d  31043  cdleme7e  31044  cdleme7ga  31045  cdleme7  31046  cdleme11l  31066  cdleme11  31067  cdleme14  31070  cdleme15a  31071  cdleme15b  31072  cdleme15  31075  cdleme16b  31076  cdleme16c  31077  cdleme16d  31078  cdleme18d  31092  cdleme19b  31101  cdleme19e  31104  cdleme20d  31109  cdleme20g  31112  cdleme20h  31113  cdleme20i  31114  cdleme20j  31115  cdleme20l2  31118  cdleme20l  31119  cdleme20m  31120  cdleme21d  31127  cdleme21e  31128  cdleme21h  31131  cdleme22f  31143  cdleme23a  31146  cdleme23b  31147  cdleme23c  31148  cdleme24  31149  cdleme25a  31150  cdleme25dN  31153  cdleme26ee  31157  cdleme26fALTN  31159  cdleme26f  31160  cdleme26f2ALTN  31161  cdleme26f2  31162  cdleme27a  31164  cdlemefr29bpre0N  31203  cdlemefr29clN  31204  cdlemefr32fvaN  31206  cdlemefr32fva1  31207  cdleme41sn3a  31230  cdleme35a  31245  cdleme35fnpq  31246  cdleme35b  31247  cdleme35c  31248  cdleme35d  31249  cdleme35f  31251  cdleme36m  31258  cdleme37m  31259  cdleme39n  31263  cdleme43bN  31287  cdleme43dN  31289  cdleme17d2  31292  cdlemeg46c  31310  cdlemeg46nlpq  31314  cdlemeg46ngfr  31315  cdlemeg46req  31326  cdlemeg46gfv  31327  cdleme50trn1  31346  cdleme50trn2a  31347  cdlemf1  31358  cdlemf  31360  cdlemg10a  31437  cdlemg10  31438  cdlemg12d  31443  cdlemg12e  31444  cdlemg12f  31445  cdlemg12g  31446  cdlemg12  31447  cdlemg13  31449  cdlemg16ALTN  31455  cdlemg17b  31459  cdlemg17h  31465  cdlemg17pq  31469  cdlemg17iqN  31471  cdlemg17  31474  cdlemg19a  31480  cdlemg19  31481  cdlemg21  31483  cdlemg27a  31489  cdlemg27b  31493  cdlemg31c  31496  cdlemg33b0  31498  cdlemg33a  31503  cdlemg48  31534  tendocan  31621  cdlemk26-3  31703  cdlemk27-3  31704  cdlemk28-3  31705  cdlemk37  31711  cdlemky  31723  cdlemkyu  31724  cdlemk11ta  31726  cdlemkid3N  31730  cdlemk42  31738  cdlemk42yN  31741  cdlemk11t  31743  cdlemk45  31744  cdlemk46  31745  cdlemk47  31746  cdlemk51  31750  cdlemk52  31751  cdlemk53a  31752  cdleml4N  31776  dihord2pre2  32024  dihord4  32056  dihord5apre  32060  dihmeetlem1N  32088  dihmeetlem15N  32119  mapdpglem32  32503
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator