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

Theorem simpl22 1034
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl22  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ps )

Proof of Theorem simpl22
StepHypRef Expression
1 simp22 989 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
21adantr 451 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  br8  24113  brbtwn2  24533  ax5seg  24566  axpasch  24569  axeuclid  24591  cgrextend  24631  segconeq  24633  trisegint  24651  ifscgr  24667  cgrsub  24668  cgrxfr  24678  lineext  24699  seglecgr12im  24733  segletr  24737  lineunray  24770  lineelsb2  24771  isconcl5a  26101  cvrcmp  29473  cvlatexch3  29528  cvlsupr2  29533  atcvrj2b  29621  atexchcvrN  29629  3dim1  29656  3dim2  29657  3atlem3  29674  3atlem5  29676  lplnnle2at  29730  2llnjaN  29755  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  trlval4  30377  arglem1N  30379  cdlemd4  30390  cdlemd5  30391  cdleme0moN  30414  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  cdlemg16  30846  cdlemg16ALTN  30847  cdlemg16z  30848  cdlemg16zz  30849  cdlemg18a  30867  cdlemg20  30874  cdlemg22  30876  cdlemg37  30878  cdlemg31d  30889  cdlemg33  30900  cdlemg38  30904  cdlemg44b  30921  cdlemk38  31104  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk53b  31145  cdlemk55  31150  cdlemk35u  31153  cdlemk55u  31155  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