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

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

Proof of Theorem simp11r
StepHypRef Expression
1 simp1r 1019 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant1 1015 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  pceu  14372  maduf  19228  nllyrest  20072  limsupre  31813  exatleN  35541  2llnjaN  35703  2lplnja  35756  dalemceb  35775  pclfinN  36037  lhpexle3lem  36148  lhpmcvr5N  36164  lhpmcvr6N  36165  lhp2at0  36169  4atexlemw  36185  cdlemd2  36337  cdlemd4  36339  cdleme7aa  36380  cdleme7c  36383  cdleme7d  36384  cdleme7e  36385  cdleme7ga  36386  cdleme7  36387  cdleme15a  36412  cdleme15b  36413  cdleme15d  36415  cdleme15  36416  cdleme16b  36417  cdleme16c  36418  cdleme16d  36419  cdleme16e  36420  cdleme16f  36421  cdleme18d  36433  cdleme19b  36443  cdleme19d  36445  cdleme19e  36446  cdleme20d  36451  cdleme20e  36452  cdleme20f  36453  cdleme20g  36454  cdleme20h  36455  cdleme20j  36457  cdleme20k  36458  cdleme20l1  36459  cdleme20l2  36460  cdleme20l  36461  cdleme20m  36462  cdleme21c  36466  cdleme21ct  36468  cdleme22cN  36481  cdleme22f  36485  cdleme22g  36487  cdleme23a  36488  cdleme23b  36489  cdleme23c  36490  cdleme25a  36492  cdleme25c  36494  cdleme25dN  36495  cdleme26ee  36499  cdleme26eALTN  36500  cdleme27N  36508  cdleme28a  36509  cdleme28b  36510  cdleme29ex  36513  cdlemefr29exN  36541  cdleme32b  36581  cdleme32c  36582  cdleme32e  36584  cdleme35b  36589  cdleme35c  36590  cdleme35d  36591  cdleme35e  36592  cdleme35f  36593  cdleme42h  36621  cdleme42i  36622  cdleme42k  36623  cdleme48bw  36641  cdlemeg46frv  36664  cdlemeg46vrg  36666  cdlemeg46rgv  36667  cdlemeg46req  36668  cdlemf1  36700  trlord  36708  cdlemg7fvbwN  36746  cdlemg10  36780  cdlemg12e  36786  cdlemg12f  36787  cdlemg19a  36822  cdlemg31c  36838  cdlemg33c0  36841  cdlemg35  36852  tendococl  36911  cdlemh2  36955  cdlemh  36956  cdlemi  36959  cdlemk5  36975  cdlemk7  36987  cdlemk11  36988  cdlemk5u  37000  cdlemkj  37002  cdlemkuv2  37006  cdlemk7u  37009  cdlemk11u  37010  cdlemk26-3  37045  cdlemk11t  37085  cdlemk52  37093  cdlemk53a  37094  dihord1  37358  dihord2a  37359  dihord2b  37360  dihord11b  37362  dihord11c  37364  dihord2pre  37365  dihord2pre2  37366  dihord5apre  37402  dihmeetlem1N  37430  dihglblem2N  37434  dihglblem3N  37435  dihglbcpreN  37440  dihmeetlem3N  37445  dihjatc1  37451
  Copyright terms: Public domain W3C validator