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

Theorem bnj252 34141
Description:  /\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
bnj252  |-  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ph  /\  ( ps  /\  ch  /\ 
th ) ) )

Proof of Theorem bnj252
StepHypRef Expression
1 bnj250 34139 . 2  |-  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ph  /\  ( ( ps  /\  ch )  /\  th )
) )
2 df-3an 973 . . 3  |-  ( ( ps  /\  ch  /\  th )  <->  ( ( ps 
/\  ch )  /\  th ) )
32anbi2i 692 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  <->  ( ph  /\  ( ( ps  /\  ch )  /\  th )
) )
41, 3bitr4i 252 1  |-  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ph  /\  ( ps  /\  ch  /\ 
th ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    /\ w3a 971    /\ w-bnj17 34124
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 369  df-3an 973  df-bnj17 34125
This theorem is referenced by:  bnj290  34148  bnj563  34186  bnj919  34211  bnj976  34222  bnj543  34337  bnj570  34349  bnj594  34356  bnj916  34377  bnj917  34378  bnj964  34387  bnj983  34395  bnj984  34396  bnj998  34400  bnj999  34401  bnj1021  34408  bnj1083  34420  bnj1450  34492
  Copyright terms: Public domain W3C validator