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

Theorem simpl23 1035
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 990 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
21adantr 451 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  mulgdirlem  14591  br8  24113  brbtwn2  24533  ax5seglem3a  24558  ax5seg  24566  axpasch  24569  axeuclid  24591  cgrextend  24631  segconeq  24633  segconeu  24634  trisegint  24651  ifscgr  24667  cgrsub  24668  cgrxfr  24678  lineext  24699  seglecgr12im  24733  segletr  24737  lineunray  24770  lineelsb2  24771  isconcl5a  26101  cvrcmp  29473  cvlsupr2  29533  atcvrj2b  29621  atexchcvrN  29629  3atlem3  29674  3atlem5  29676  lplnnle2at  29730  lplnllnneN  29745  4atlem3  29785  4atlem10b  29794  4atlem12  29801  2llnma3r  29977  paddasslem4  30012  paddasslem7  30015  paddasslem8  30016  paddasslem12  30020  paddasslem13  30021  paddasslem15  30023  pmodlem1  30035  pmodlem2  30036  atmod1i1m  30047  llnexchb2lem  30057  4atex2  30266  ltrnatlw  30372  arglem1N  30379  cdlemd4  30390  cdlemd5  30391  cdleme16  30474  cdleme20  30513  cdleme21k  30527  cdleme27N  30558  cdleme28c  30561  cdleme43fsv1snlem  30609  cdleme38n  30653  cdleme40n  30657  cdleme41snaw  30665  cdlemg6c  30809  cdlemg8c  30818  cdlemg8  30820  cdlemg12e  30836  cdlemg16ALTN  30847  cdlemg16zz  30849  cdlemg18a  30867  cdlemg20  30874  cdlemg22  30876  cdlemg37  30878  cdlemg31d  30889  cdlemg33  30900  cdlemg38  30904  cdlemg44b  30921  cdlemk33N  31098  cdlemk34  31099  cdlemk38  31104  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk53b  31145  cdlemk53  31146  cdlemk55  31150  cdlemk35u  31153  cdlemk55u  31155  cdleml3N  31167  cdlemn11pre  31400
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator