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

Theorem simpl23 1038
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 993 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
21adantr 453 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  mulgdirlem  14916  br8  25381  brbtwn2  25846  ax5seglem3a  25871  ax5seg  25879  axpasch  25882  axeuclid  25904  cgrextend  25944  segconeq  25946  segconeu  25947  trisegint  25964  ifscgr  25980  cgrsub  25981  cgrxfr  25991  lineext  26012  seglecgr12im  26046  segletr  26050  lineunray  26083  lineelsb2  26084  cvrcmp  30143  cvlsupr2  30203  atcvrj2b  30291  atexchcvrN  30299  3atlem3  30344  3atlem5  30346  lplnnle2at  30400  lplnllnneN  30415  4atlem3  30455  4atlem10b  30464  4atlem12  30471  2llnma3r  30647  paddasslem4  30682  paddasslem7  30685  paddasslem8  30686  paddasslem12  30690  paddasslem13  30691  paddasslem15  30693  pmodlem1  30705  pmodlem2  30706  atmod1i1m  30717  llnexchb2lem  30727  4atex2  30936  ltrnatlw  31042  arglem1N  31049  cdlemd4  31060  cdlemd5  31061  cdleme16  31144  cdleme20  31183  cdleme21k  31197  cdleme27N  31228  cdleme28c  31231  cdleme43fsv1snlem  31279  cdleme38n  31323  cdleme40n  31327  cdleme41snaw  31335  cdlemg6c  31479  cdlemg8c  31488  cdlemg8  31490  cdlemg12e  31506  cdlemg16ALTN  31517  cdlemg16zz  31519  cdlemg18a  31537  cdlemg20  31544  cdlemg22  31546  cdlemg37  31548  cdlemg31d  31559  cdlemg33  31570  cdlemg38  31574  cdlemg44b  31591  cdlemk33N  31768  cdlemk34  31769  cdlemk38  31774  cdlemk35s-id  31797  cdlemk39s-id  31799  cdlemk53b  31815  cdlemk53  31816  cdlemk55  31820  cdlemk35u  31823  cdlemk55u  31825  cdleml3N  31837  cdlemn11pre  32070
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator