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

Theorem simp13l 1103
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 1016 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant1 1009 1  |-  ( ( ( ch  /\  th  /\  ( ph  /\  ps ) )  /\  ta  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  pceu  14030  axpasch  23338  mzpcong  29462  3atlem4  33453  llncvrlpln2  33524  2lplnja  33586  2lnat  33751  llnexchb2  33836  lhp2lt  33968  lhpmcvr5N  33994  4atexlemq  34018  4atexlemex6  34041  trlval2  34130  cdleme7d  34213  cdleme7e  34214  cdleme7ga  34215  cdleme7  34216  cdleme11l  34236  cdleme11  34237  cdleme14  34240  cdleme15a  34241  cdleme15b  34242  cdleme15  34245  cdleme16b  34246  cdleme16c  34247  cdleme16d  34248  cdleme18d  34262  cdleme19b  34271  cdleme19e  34274  cdleme20d  34279  cdleme20g  34282  cdleme20h  34283  cdleme20i  34284  cdleme20j  34285  cdleme20l2  34288  cdleme20l  34289  cdleme20m  34290  cdleme21d  34297  cdleme21e  34298  cdleme21h  34301  cdleme22f  34313  cdleme23a  34316  cdleme23b  34317  cdleme23c  34318  cdleme24  34319  cdleme25a  34320  cdleme25dN  34323  cdleme26ee  34327  cdleme26fALTN  34329  cdleme26f  34330  cdleme26f2ALTN  34331  cdleme26f2  34332  cdleme27a  34334  cdlemefr29bpre0N  34373  cdlemefr29clN  34374  cdlemefr32fvaN  34376  cdlemefr32fva1  34377  cdleme41sn3a  34400  cdleme35a  34415  cdleme35fnpq  34416  cdleme35b  34417  cdleme35c  34418  cdleme35d  34419  cdleme35f  34421  cdleme36m  34428  cdleme37m  34429  cdleme39n  34433  cdleme43bN  34457  cdleme43dN  34459  cdleme17d2  34462  cdlemeg46c  34480  cdlemeg46nlpq  34484  cdlemeg46ngfr  34485  cdlemeg46req  34496  cdlemeg46gfv  34497  cdleme50trn1  34516  cdleme50trn2a  34517  cdlemf1  34528  cdlemf  34530  cdlemg10a  34607  cdlemg10  34608  cdlemg12d  34613  cdlemg12e  34614  cdlemg12f  34615  cdlemg12g  34616  cdlemg12  34617  cdlemg13  34619  cdlemg16ALTN  34625  cdlemg17b  34629  cdlemg17h  34635  cdlemg17pq  34639  cdlemg17iqN  34641  cdlemg17  34644  cdlemg19a  34650  cdlemg19  34651  cdlemg21  34653  cdlemg27a  34659  cdlemg27b  34663  cdlemg31c  34666  cdlemg33b0  34668  cdlemg33a  34673  cdlemg48  34704  tendocan  34791  cdlemk26-3  34873  cdlemk27-3  34874  cdlemk28-3  34875  cdlemk37  34881  cdlemky  34893  cdlemkyu  34894  cdlemk11ta  34896  cdlemkid3N  34900  cdlemk42  34908  cdlemk42yN  34911  cdlemk11t  34913  cdlemk45  34914  cdlemk46  34915  cdlemk47  34916  cdlemk51  34920  cdlemk52  34921  cdlemk53a  34922  cdleml4N  34946  dihord2pre2  35194  dihord4  35226  dihord5apre  35230  dihmeetlem1N  35258  dihmeetlem15N  35289  mapdpglem32  35673
  Copyright terms: Public domain W3C validator