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

Theorem simpl21 1035
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 990 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ph )
21adantr 452 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  br8  25335  brbtwn2  25756  ax5seglem3a  25781  ax5seg  25789  axpasch  25792  axeuclid  25814  cgrextend  25854  segconeq  25856  trisegint  25874  ifscgr  25890  cgrsub  25891  cgrxfr  25901  lineext  25922  seglecgr12im  25956  segletr  25960  lineunray  25993  lineelsb2  25994  cvrcmp  29778  cvlatexch3  29833  cvlsupr2  29838  atexchcvrN  29934  3dim1  29961  3dim2  29962  ps-1  29971  ps-2  29972  3atlem3  29979  3atlem5  29981  lplnnle2at  30035  lplnllnneN  30050  2llnjaN  30060  4atlem3  30090  4atlem10b  30099  4atlem12  30106  2llnma3r  30282  paddasslem4  30317  paddasslem7  30320  paddasslem8  30321  paddasslem12  30325  paddasslem13  30326  pmodlem1  30340  pmodlem2  30341  llnexchb2lem  30362  4atex2  30571  ltrnatlw  30677  trlval4  30682  arglem1N  30684  cdlemd4  30695  cdlemd5  30696  cdleme0moN  30719  cdleme16  30779  cdleme20  30818  cdleme21j  30830  cdleme21k  30832  cdleme27N  30863  cdleme28c  30866  cdleme43fsv1snlem  30914  cdleme38n  30958  cdleme40n  30962  cdleme41snaw  30970  cdlemg6c  31114  cdlemg8c  31123  cdlemg8  31125  cdlemg12e  31141  cdlemg16  31151  cdlemg16ALTN  31152  cdlemg16z  31153  cdlemg16zz  31154  cdlemg18a  31172  cdlemg20  31179  cdlemg22  31181  cdlemg37  31183  cdlemg27b  31190  cdlemg31d  31194  cdlemg33  31205  cdlemg38  31209  cdlemg44b  31226  cdlemk38  31409  cdlemk35s-id  31432  cdlemk39s-id  31434  cdlemk55  31455  cdlemk35u  31458  cdlemk55u  31460  cdleml3N  31472  cdlemn11pre  31705
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