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

Theorem bnj252 29044
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 29042 . 2  |-  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ph  /\  ( ( ps  /\  ch )  /\  th )
) )
2 df-3an 936 . . 3  |-  ( ( ps  /\  ch  /\  th )  <->  ( ( ps 
/\  ch )  /\  th ) )
32anbi2i 675 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  <->  ( ph  /\  ( ( ps  /\  ch )  /\  th )
) )
41, 3bitr4i 243 1  |-  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ph  /\  ( ps  /\  ch  /\ 
th ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    /\ w3a 934    /\ w-bnj17 29027
This theorem is referenced by:  bnj290  29051  bnj563  29088  bnj919  29113  bnj976  29125  bnj543  29241  bnj570  29253  bnj594  29260  bnj916  29281  bnj917  29282  bnj964  29291  bnj983  29299  bnj984  29300  bnj998  29304  bnj999  29305  bnj1021  29312  bnj1083  29324  bnj1450  29396
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 177  df-an 360  df-3an 936  df-bnj17 29028
  Copyright terms: Public domain W3C validator