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

Theorem bnj835 32054
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 1009 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
41, 3sylbi 195 1  |-  ( et 
->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 965
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 967
This theorem is referenced by:  bnj1219  32096  bnj1379  32126  bnj1175  32297  bnj1286  32312  bnj1280  32313  bnj1296  32314  bnj1398  32327  bnj1415  32331  bnj1417  32334  bnj1421  32335  bnj1442  32342  bnj1450  32343  bnj1452  32345  bnj1489  32349  bnj1312  32351  bnj1501  32360  bnj1523  32364
  Copyright terms: Public domain W3C validator