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

Theorem simp11r 1119
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 1032 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant1 1028 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 984
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 189  df-an 373  df-3an 986
This theorem is referenced by:  pceu  14789  maduf  19659  nllyrest  20494  exatleN  32963  2llnjaN  33125  2lplnja  33178  dalemceb  33197  pclfinN  33459  lhpexle3lem  33570  lhpmcvr5N  33586  lhpmcvr6N  33587  lhp2at0  33591  4atexlemw  33607  cdlemd2  33759  cdlemd4  33761  cdleme7aa  33802  cdleme7c  33805  cdleme7d  33806  cdleme7e  33807  cdleme7ga  33808  cdleme7  33809  cdleme15a  33834  cdleme15b  33835  cdleme15d  33837  cdleme15  33838  cdleme16b  33839  cdleme16c  33840  cdleme16d  33841  cdleme16e  33842  cdleme16f  33843  cdleme18d  33855  cdleme19b  33865  cdleme19d  33867  cdleme19e  33868  cdleme20d  33873  cdleme20e  33874  cdleme20f  33875  cdleme20g  33876  cdleme20h  33877  cdleme20j  33879  cdleme20k  33880  cdleme20l1  33881  cdleme20l2  33882  cdleme20l  33883  cdleme20m  33884  cdleme21c  33888  cdleme21ct  33890  cdleme22cN  33903  cdleme22f  33907  cdleme22g  33909  cdleme23a  33910  cdleme23b  33911  cdleme23c  33912  cdleme25a  33914  cdleme25c  33916  cdleme25dN  33917  cdleme26ee  33921  cdleme26eALTN  33922  cdleme27N  33930  cdleme28a  33931  cdleme28b  33932  cdleme29ex  33935  cdlemefr29exN  33963  cdleme32b  34003  cdleme32c  34004  cdleme32e  34006  cdleme35b  34011  cdleme35c  34012  cdleme35d  34013  cdleme35e  34014  cdleme35f  34015  cdleme42h  34043  cdleme42i  34044  cdleme42k  34045  cdleme48bw  34063  cdlemeg46frv  34086  cdlemeg46vrg  34088  cdlemeg46rgv  34089  cdlemeg46req  34090  cdlemf1  34122  trlord  34130  cdlemg7fvbwN  34168  cdlemg10  34202  cdlemg12e  34208  cdlemg12f  34209  cdlemg19a  34244  cdlemg31c  34260  cdlemg33c0  34263  cdlemg35  34274  tendococl  34333  cdlemh2  34377  cdlemh  34378  cdlemi  34381  cdlemk5  34397  cdlemk7  34409  cdlemk11  34410  cdlemk5u  34422  cdlemkj  34424  cdlemkuv2  34428  cdlemk7u  34431  cdlemk11u  34432  cdlemk26-3  34467  cdlemk11t  34507  cdlemk52  34515  cdlemk53a  34516  dihord1  34780  dihord2a  34781  dihord2b  34782  dihord11b  34784  dihord11c  34786  dihord2pre  34787  dihord2pre2  34788  dihord5apre  34824  dihmeetlem1N  34852  dihglblem2N  34856  dihglblem3N  34857  dihglbcpreN  34862  dihmeetlem3N  34867  dihjatc1  34873  suplesup  37556  limsupre  37715  limsupreOLD  37716  sge0xaddlem2  38270
  Copyright terms: Public domain W3C validator