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

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

Proof of Theorem simpl13
StepHypRef Expression
1 simp13 1040 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ch )
21adantr 467 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  pythagtriplem4  14769  mply1topmatcl  19829  brbtwn2  24935  ax5seg  24968  br8  30396  btwndiff  30794  ifscgr  30811  seglecgr12im  30877  atlatle  32886  cvlcvr1  32905  atbtwn  33011  3dimlem3  33026  3dimlem3OLDN  33027  4atlem3  33161  4atlem11  33174  4atlem12  33177  2lplnj  33185  paddasslem4  33388  paddasslem10  33394  pmodlem1  33411  llnexchb2lem  33433  pclfinclN  33515  arglem1N  33756  cdlemd4  33767  cdlemd  33773  cdleme16  33851  cdleme20  33891  cdleme21k  33905  cdleme22cN  33909  cdleme27N  33936  cdleme28c  33939  cdleme29ex  33941  cdleme32fva  34004  cdleme40n  34035  cdlemg15a  34222  cdlemg15  34223  cdlemg16ALTN  34225  cdlemg16z  34226  cdlemg20  34252  cdlemg22  34254  cdlemg29  34272  cdlemg38  34282  cdlemk56  34538  dihord2pre  34793  uzwo4  37392  fourierdlem77  38047
  Copyright terms: Public domain W3C validator