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

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

Proof of Theorem simpl23
StepHypRef Expression
1 simp23 1042 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
21adantr 467 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ch )
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:  mulgdirlem  16775  brbtwn2  24928  ax5seglem3a  24953  ax5seg  24961  axpasch  24964  axeuclid  24986  br8d  28211  br8  30389  cgrextend  30768  segconeq  30770  segconeu  30771  trisegint  30788  ifscgr  30804  cgrsub  30805  cgrxfr  30815  lineext  30836  seglecgr12im  30870  segletr  30874  lineunray  30907  lineelsb2  30908  cvrcmp  32843  cvlsupr2  32903  atcvrj2b  32991  atexchcvrN  32999  3atlem3  33044  3atlem5  33046  lplnnle2at  33100  lplnllnneN  33115  4atlem3  33155  4atlem10b  33164  4atlem12  33171  2llnma3r  33347  paddasslem4  33382  paddasslem7  33385  paddasslem8  33386  paddasslem12  33390  paddasslem13  33391  paddasslem15  33393  pmodlem1  33405  pmodlem2  33406  atmod1i1m  33417  llnexchb2lem  33427  4atex2  33636  ltrnatlw  33743  arglem1N  33750  cdlemd4  33761  cdlemd5  33762  cdleme16  33845  cdleme20  33885  cdleme21k  33899  cdleme27N  33930  cdleme28c  33933  cdleme43fsv1snlem  33981  cdleme38n  34025  cdleme40n  34029  cdleme41snaw  34037  cdlemg6c  34181  cdlemg8c  34190  cdlemg8  34192  cdlemg12e  34208  cdlemg16ALTN  34219  cdlemg16zz  34221  cdlemg18a  34239  cdlemg20  34246  cdlemg22  34248  cdlemg37  34250  cdlemg31d  34261  cdlemg33  34272  cdlemg38  34276  cdlemg44b  34293  cdlemk33N  34470  cdlemk34  34471  cdlemk38  34476  cdlemk35s-id  34499  cdlemk39s-id  34501  cdlemk53b  34517  cdlemk53  34518  cdlemk55  34522  cdlemk35u  34525  cdlemk55u  34527  cdleml3N  34539  cdlemn11pre  34772
  Copyright terms: Public domain W3C validator