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 32896
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 1017 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
41, 3sylbi 195 1  |-  ( et 
->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973
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 975
This theorem is referenced by:  bnj1219  32938  bnj1379  32968  bnj1175  33139  bnj1286  33154  bnj1280  33155  bnj1296  33156  bnj1398  33169  bnj1415  33173  bnj1417  33176  bnj1421  33177  bnj1442  33184  bnj1450  33185  bnj1452  33187  bnj1489  33191  bnj1312  33193  bnj1501  33202  bnj1523  33206
  Copyright terms: Public domain W3C validator