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

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

Proof of Theorem simpl21
StepHypRef Expression
1 simp21 988 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ph )
21adantr 451 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  br8  24113  brbtwn2  24533  ax5seglem3a  24558  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  atexchcvrN  29629  3dim1  29656  3dim2  29657  ps-1  29666  ps-2  29667  3atlem3  29674  3atlem5  29676  lplnnle2at  29730  lplnllnneN  29745  2llnjaN  29755  4atlem3  29785  4atlem10b  29794  4atlem12  29801  2llnma3r  29977  paddasslem4  30012  paddasslem7  30015  paddasslem8  30016  paddasslem12  30020  paddasslem13  30021  pmodlem1  30035  pmodlem2  30036  llnexchb2lem  30057  4atex2  30266  ltrnatlw  30372  trlval4  30377  arglem1N  30379  cdlemd4  30390  cdlemd5  30391  cdleme0moN  30414  cdleme16  30474  cdleme20  30513  cdleme21j  30525  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  cdlemg27b  30885  cdlemg31d  30889  cdlemg33  30900  cdlemg38  30904  cdlemg44b  30921  cdlemk38  31104  cdlemk35s-id  31127  cdlemk39s-id  31129  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