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

Theorem simpl23 1076
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 1031 . 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 973
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 975
This theorem is referenced by:  mulgdirlem  16293  brbtwn2  24335  ax5seglem3a  24360  ax5seg  24368  axpasch  24371  axeuclid  24393  br8d  27606  br8  29382  cgrextend  29842  segconeq  29844  segconeu  29845  trisegint  29862  ifscgr  29878  cgrsub  29879  cgrxfr  29889  lineext  29910  seglecgr12im  29944  segletr  29948  lineunray  29981  lineelsb2  29982  cvrcmp  35130  cvlsupr2  35190  atcvrj2b  35278  atexchcvrN  35286  3atlem3  35331  3atlem5  35333  lplnnle2at  35387  lplnllnneN  35402  4atlem3  35442  4atlem10b  35451  4atlem12  35458  2llnma3r  35634  paddasslem4  35669  paddasslem7  35672  paddasslem8  35673  paddasslem12  35677  paddasslem13  35678  paddasslem15  35680  pmodlem1  35692  pmodlem2  35693  atmod1i1m  35704  llnexchb2lem  35714  4atex2  35923  ltrnatlw  36030  arglem1N  36037  cdlemd4  36048  cdlemd5  36049  cdleme16  36132  cdleme20  36172  cdleme21k  36186  cdleme27N  36217  cdleme28c  36220  cdleme43fsv1snlem  36268  cdleme38n  36312  cdleme40n  36316  cdleme41snaw  36324  cdlemg6c  36468  cdlemg8c  36477  cdlemg8  36479  cdlemg12e  36495  cdlemg16ALTN  36506  cdlemg16zz  36508  cdlemg18a  36526  cdlemg20  36533  cdlemg22  36535  cdlemg37  36537  cdlemg31d  36548  cdlemg33  36559  cdlemg38  36563  cdlemg44b  36580  cdlemk33N  36757  cdlemk34  36758  cdlemk38  36763  cdlemk35s-id  36786  cdlemk39s-id  36788  cdlemk53b  36804  cdlemk53  36805  cdlemk55  36809  cdlemk35u  36812  cdlemk55u  36814  cdleml3N  36826  cdlemn11pre  37059
  Copyright terms: Public domain W3C validator