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  24184  brbtwn2  24605  ax5seglem3a  24630  ax5seg  24638  axpasch  24641  axeuclid  24663  cgrextend  24703  segconeq  24705  trisegint  24723  ifscgr  24739  cgrsub  24740  cgrxfr  24750  lineext  24771  seglecgr12im  24805  segletr  24809  lineunray  24842  lineelsb2  24843  isconcl5a  26204  cvrcmp  30095  cvlatexch3  30150  cvlsupr2  30155  atexchcvrN  30251  3dim1  30278  3dim2  30279  ps-1  30288  ps-2  30289  3atlem3  30296  3atlem5  30298  lplnnle2at  30352  lplnllnneN  30367  2llnjaN  30377  4atlem3  30407  4atlem10b  30416  4atlem12  30423  2llnma3r  30599  paddasslem4  30634  paddasslem7  30637  paddasslem8  30638  paddasslem12  30642  paddasslem13  30643  pmodlem1  30657  pmodlem2  30658  llnexchb2lem  30679  4atex2  30888  ltrnatlw  30994  trlval4  30999  arglem1N  31001  cdlemd4  31012  cdlemd5  31013  cdleme0moN  31036  cdleme16  31096  cdleme20  31135  cdleme21j  31147  cdleme21k  31149  cdleme27N  31180  cdleme28c  31183  cdleme43fsv1snlem  31231  cdleme38n  31275  cdleme40n  31279  cdleme41snaw  31287  cdlemg6c  31431  cdlemg8c  31440  cdlemg8  31442  cdlemg12e  31458  cdlemg16  31468  cdlemg16ALTN  31469  cdlemg16z  31470  cdlemg16zz  31471  cdlemg18a  31489  cdlemg20  31496  cdlemg22  31498  cdlemg37  31500  cdlemg27b  31507  cdlemg31d  31511  cdlemg33  31522  cdlemg38  31526  cdlemg44b  31543  cdlemk38  31726  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk55  31772  cdlemk35u  31775  cdlemk55u  31777  cdleml3N  31789  cdlemn11pre  32022
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