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 29349
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 1026 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
41, 3sylbi 198 1  |-  ( et 
->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  bnj1219  29391  bnj1379  29421  bnj1175  29592  bnj1286  29607  bnj1280  29608  bnj1296  29609  bnj1398  29622  bnj1415  29626  bnj1417  29629  bnj1421  29630  bnj1442  29637  bnj1450  29638  bnj1452  29640  bnj1489  29644  bnj1312  29646  bnj1501  29655  bnj1523  29659
  Copyright terms: Public domain W3C validator