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

Theorem bnj252 28728
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 28726 . 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 28711
This theorem is referenced by:  bnj290  28735  bnj563  28772  bnj919  28797  bnj976  28809  bnj543  28925  bnj570  28937  bnj594  28944  bnj916  28965  bnj917  28966  bnj964  28975  bnj983  28983  bnj984  28984  bnj998  28988  bnj999  28989  bnj1021  28996  bnj1083  29008  bnj1450  29080
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 28712
  Copyright terms: Public domain W3C validator