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

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

Proof of Theorem simpl31
StepHypRef Expression
1 simp31 993 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ph )
21adantr 452 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  br8  25371  ax5seglem3a  25861  ax5seg  25869  cgrextend  25934  segconeq  25936  trisegint  25954  ifscgr  25970  cgrsub  25971  btwnxfr  25982  seglecgr12im  26036  segletr  26040  atbtwn  30170  3dim1  30191  2llnjaN  30290  4atlem10b  30329  4atlem11  30333  4atlem12  30336  2lplnj  30344  paddasslem4  30547  pmodlem1  30570  4atex2  30801  trlval3  30911  arglem1N  30914  cdleme0moN  30949  cdleme17b  31011  cdleme20  31048  cdleme21j  31060  cdleme28c  31096  cdleme35h2  31181  cdlemg6c  31344  cdlemg6  31347  cdlemg7N  31350  cdlemg8c  31353  cdlemg11a  31361  cdlemg11b  31366  cdlemg12e  31371  cdlemg16  31381  cdlemg16ALTN  31382  cdlemg16zz  31384  cdlemg20  31409  cdlemg22  31411  cdlemg37  31413  cdlemg31d  31424  cdlemg33b  31431  cdlemg33  31435  cdlemg39  31440  cdlemg42  31453  cdlemk25-3  31628  cdlemk33N  31633  cdlemk53b  31680
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