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

Theorem simpl23 1063
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 1018 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
21adantr 462 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 185  df-an 371  df-3an 962
This theorem is referenced by:  mulgdirlem  15644  brbtwn2  23070  ax5seglem3a  23095  ax5seg  23103  axpasch  23106  axeuclid  23128  br8d  25861  br8  27479  cgrextend  27952  segconeq  27954  segconeu  27955  trisegint  27972  ifscgr  27988  cgrsub  27989  cgrxfr  27999  lineext  28020  seglecgr12im  28054  segletr  28058  lineunray  28091  lineelsb2  28092  cvrcmp  32616  cvlsupr2  32676  atcvrj2b  32764  atexchcvrN  32772  3atlem3  32817  3atlem5  32819  lplnnle2at  32873  lplnllnneN  32888  4atlem3  32928  4atlem10b  32937  4atlem12  32944  2llnma3r  33120  paddasslem4  33155  paddasslem7  33158  paddasslem8  33159  paddasslem12  33163  paddasslem13  33164  paddasslem15  33166  pmodlem1  33178  pmodlem2  33179  atmod1i1m  33190  llnexchb2lem  33200  4atex2  33409  ltrnatlw  33515  arglem1N  33522  cdlemd4  33533  cdlemd5  33534  cdleme16  33617  cdleme20  33656  cdleme21k  33670  cdleme27N  33701  cdleme28c  33704  cdleme43fsv1snlem  33752  cdleme38n  33796  cdleme40n  33800  cdleme41snaw  33808  cdlemg6c  33952  cdlemg8c  33961  cdlemg8  33963  cdlemg12e  33979  cdlemg16ALTN  33990  cdlemg16zz  33992  cdlemg18a  34010  cdlemg20  34017  cdlemg22  34019  cdlemg37  34021  cdlemg31d  34032  cdlemg33  34043  cdlemg38  34047  cdlemg44b  34064  cdlemk33N  34241  cdlemk34  34242  cdlemk38  34247  cdlemk35s-id  34270  cdlemk39s-id  34272  cdlemk53b  34288  cdlemk53  34289  cdlemk55  34293  cdlemk35u  34296  cdlemk55u  34298  cdleml3N  34310  cdlemn11pre  34543
  Copyright terms: Public domain W3C validator