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 29128
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 978 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
41, 3sylbi 188 1  |-  ( et 
->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  bnj1219  29172  bnj1379  29202  bnj1175  29373  bnj1286  29388  bnj1280  29389  bnj1296  29390  bnj1398  29403  bnj1415  29407  bnj1417  29410  bnj1421  29411  bnj1442  29418  bnj1450  29419  bnj1452  29421  bnj1489  29425  bnj1312  29427  bnj1501  29436  bnj1523  29440
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator