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

Theorem simpl23 1071
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 1026 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
21adantr 465 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 970
This theorem is referenced by:  mulgdirlem  15959  brbtwn2  23877  ax5seglem3a  23902  ax5seg  23910  axpasch  23913  axeuclid  23935  br8d  27122  br8  28748  cgrextend  29221  segconeq  29223  segconeu  29224  trisegint  29241  ifscgr  29257  cgrsub  29258  cgrxfr  29268  lineext  29289  seglecgr12im  29323  segletr  29327  lineunray  29360  lineelsb2  29361  cvrcmp  33955  cvlsupr2  34015  atcvrj2b  34103  atexchcvrN  34111  3atlem3  34156  3atlem5  34158  lplnnle2at  34212  lplnllnneN  34227  4atlem3  34267  4atlem10b  34276  4atlem12  34283  2llnma3r  34459  paddasslem4  34494  paddasslem7  34497  paddasslem8  34498  paddasslem12  34502  paddasslem13  34503  paddasslem15  34505  pmodlem1  34517  pmodlem2  34518  atmod1i1m  34529  llnexchb2lem  34539  4atex2  34748  ltrnatlw  34854  arglem1N  34861  cdlemd4  34872  cdlemd5  34873  cdleme16  34956  cdleme20  34995  cdleme21k  35009  cdleme27N  35040  cdleme28c  35043  cdleme43fsv1snlem  35091  cdleme38n  35135  cdleme40n  35139  cdleme41snaw  35147  cdlemg6c  35291  cdlemg8c  35300  cdlemg8  35302  cdlemg12e  35318  cdlemg16ALTN  35329  cdlemg16zz  35331  cdlemg18a  35349  cdlemg20  35356  cdlemg22  35358  cdlemg37  35360  cdlemg31d  35371  cdlemg33  35382  cdlemg38  35386  cdlemg44b  35403  cdlemk33N  35580  cdlemk34  35581  cdlemk38  35586  cdlemk35s-id  35609  cdlemk39s-id  35611  cdlemk53b  35627  cdlemk53  35628  cdlemk55  35632  cdlemk35u  35635  cdlemk55u  35637  cdleml3N  35649  cdlemn11pre  35882
  Copyright terms: Public domain W3C validator