Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj835 Unicode version

Theorem bnj835 28300
Description:  /\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj835.1  |-  ( et  <->  (
ph  /\  ps  /\  ch ) )
bnj835.2  |-  ( ph  ->  ta )
Assertion
Ref Expression
bnj835  |-  ( et 
->  ta )

Proof of Theorem bnj835
StepHypRef Expression
1 bnj835.1 . 2  |-  ( et  <->  (
ph  /\  ps  /\  ch ) )
2 bnj835.2 . . 3  |-  ( ph  ->  ta )
323ad2ant1 976 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
41, 3sylbi 187 1  |-  ( et 
->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  bnj1219  28344  bnj1379  28374  bnj1175  28545  bnj1286  28560  bnj1280  28561  bnj1296  28562  bnj1398  28575  bnj1415  28579  bnj1417  28582  bnj1421  28583  bnj1442  28590  bnj1450  28591  bnj1452  28593  bnj1489  28597  bnj1312  28599  bnj1501  28608  bnj1523  28612
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