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

Theorem bnj835 28789
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  28833  bnj1379  28863  bnj1175  29034  bnj1286  29049  bnj1280  29050  bnj1296  29051  bnj1398  29064  bnj1415  29068  bnj1417  29071  bnj1421  29072  bnj1442  29079  bnj1450  29080  bnj1452  29082  bnj1489  29086  bnj1312  29088  bnj1501  29097  bnj1523  29101
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