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

Theorem simpl23 1037
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 992 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
21adantr 452 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  mulgdirlem  14869  br8  25327  brbtwn2  25748  ax5seglem3a  25773  ax5seg  25781  axpasch  25784  axeuclid  25806  cgrextend  25846  segconeq  25848  segconeu  25849  trisegint  25866  ifscgr  25882  cgrsub  25883  cgrxfr  25893  lineext  25914  seglecgr12im  25948  segletr  25952  lineunray  25985  lineelsb2  25986  cvrcmp  29766  cvlsupr2  29826  atcvrj2b  29914  atexchcvrN  29922  3atlem3  29967  3atlem5  29969  lplnnle2at  30023  lplnllnneN  30038  4atlem3  30078  4atlem10b  30087  4atlem12  30094  2llnma3r  30270  paddasslem4  30305  paddasslem7  30308  paddasslem8  30309  paddasslem12  30313  paddasslem13  30314  paddasslem15  30316  pmodlem1  30328  pmodlem2  30329  atmod1i1m  30340  llnexchb2lem  30350  4atex2  30559  ltrnatlw  30665  arglem1N  30672  cdlemd4  30683  cdlemd5  30684  cdleme16  30767  cdleme20  30806  cdleme21k  30820  cdleme27N  30851  cdleme28c  30854  cdleme43fsv1snlem  30902  cdleme38n  30946  cdleme40n  30950  cdleme41snaw  30958  cdlemg6c  31102  cdlemg8c  31111  cdlemg8  31113  cdlemg12e  31129  cdlemg16ALTN  31140  cdlemg16zz  31142  cdlemg18a  31160  cdlemg20  31167  cdlemg22  31169  cdlemg37  31171  cdlemg31d  31182  cdlemg33  31193  cdlemg38  31197  cdlemg44b  31214  cdlemk33N  31391  cdlemk34  31392  cdlemk38  31397  cdlemk35s-id  31420  cdlemk39s-id  31422  cdlemk53b  31438  cdlemk53  31439  cdlemk55  31443  cdlemk35u  31446  cdlemk55u  31448  cdleml3N  31460  cdlemn11pre  31693
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator