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

Theorem simpl23 1110
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 1065 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
21adantr 472 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 190  df-an 378  df-3an 1009
This theorem is referenced by:  mulgdirlem  16860  brbtwn2  25014  ax5seglem3a  25039  ax5seg  25047  axpasch  25050  axeuclid  25072  br8d  28294  br8  30467  cgrextend  30846  segconeq  30848  segconeu  30849  trisegint  30866  ifscgr  30882  cgrsub  30883  cgrxfr  30893  lineext  30914  seglecgr12im  30948  segletr  30952  lineunray  30985  lineelsb2  30986  cvrcmp  32920  cvlsupr2  32980  atcvrj2b  33068  atexchcvrN  33076  3atlem3  33121  3atlem5  33123  lplnnle2at  33177  lplnllnneN  33192  4atlem3  33232  4atlem10b  33241  4atlem12  33248  2llnma3r  33424  paddasslem4  33459  paddasslem7  33462  paddasslem8  33463  paddasslem12  33467  paddasslem13  33468  paddasslem15  33470  pmodlem1  33482  pmodlem2  33483  atmod1i1m  33494  llnexchb2lem  33504  4atex2  33713  ltrnatlw  33820  arglem1N  33827  cdlemd4  33838  cdlemd5  33839  cdleme16  33922  cdleme20  33962  cdleme21k  33976  cdleme27N  34007  cdleme28c  34010  cdleme43fsv1snlem  34058  cdleme38n  34102  cdleme40n  34106  cdleme41snaw  34114  cdlemg6c  34258  cdlemg8c  34267  cdlemg8  34269  cdlemg12e  34285  cdlemg16ALTN  34296  cdlemg16zz  34298  cdlemg18a  34316  cdlemg20  34323  cdlemg22  34325  cdlemg37  34327  cdlemg31d  34338  cdlemg33  34349  cdlemg38  34353  cdlemg44b  34370  cdlemk33N  34547  cdlemk34  34548  cdlemk38  34553  cdlemk35s-id  34576  cdlemk39s-id  34578  cdlemk53b  34594  cdlemk53  34595  cdlemk55  34599  cdlemk35u  34602  cdlemk55u  34604  cdleml3N  34616  cdlemn11pre  34849
  Copyright terms: Public domain W3C validator