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

Theorem simpl23 1068
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 1023 . 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 965
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 967
This theorem is referenced by:  mulgdirlem  15651  brbtwn2  23151  ax5seglem3a  23176  ax5seg  23184  axpasch  23187  axeuclid  23209  br8d  25942  br8  27566  cgrextend  28039  segconeq  28041  segconeu  28042  trisegint  28059  ifscgr  28075  cgrsub  28076  cgrxfr  28086  lineext  28107  seglecgr12im  28141  segletr  28145  lineunray  28178  lineelsb2  28179  cvrcmp  32928  cvlsupr2  32988  atcvrj2b  33076  atexchcvrN  33084  3atlem3  33129  3atlem5  33131  lplnnle2at  33185  lplnllnneN  33200  4atlem3  33240  4atlem10b  33249  4atlem12  33256  2llnma3r  33432  paddasslem4  33467  paddasslem7  33470  paddasslem8  33471  paddasslem12  33475  paddasslem13  33476  paddasslem15  33478  pmodlem1  33490  pmodlem2  33491  atmod1i1m  33502  llnexchb2lem  33512  4atex2  33721  ltrnatlw  33827  arglem1N  33834  cdlemd4  33845  cdlemd5  33846  cdleme16  33929  cdleme20  33968  cdleme21k  33982  cdleme27N  34013  cdleme28c  34016  cdleme43fsv1snlem  34064  cdleme38n  34108  cdleme40n  34112  cdleme41snaw  34120  cdlemg6c  34264  cdlemg8c  34273  cdlemg8  34275  cdlemg12e  34291  cdlemg16ALTN  34302  cdlemg16zz  34304  cdlemg18a  34322  cdlemg20  34329  cdlemg22  34331  cdlemg37  34333  cdlemg31d  34344  cdlemg33  34355  cdlemg38  34359  cdlemg44b  34376  cdlemk33N  34553  cdlemk34  34554  cdlemk38  34559  cdlemk35s-id  34582  cdlemk39s-id  34584  cdlemk53b  34600  cdlemk53  34601  cdlemk55  34605  cdlemk35u  34608  cdlemk55u  34610  cdleml3N  34622  cdlemn11pre  34855
  Copyright terms: Public domain W3C validator