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 29069
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 29067 . 2  |-  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ph  /\  ( ( ps  /\  ch )  /\  th )
) )
2 df-3an 939 . . 3  |-  ( ( ps  /\  ch  /\  th )  <->  ( ( ps 
/\  ch )  /\  th ) )
32anbi2i 677 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  <->  ( ph  /\  ( ( ps  /\  ch )  /\  th )
) )
41, 3bitr4i 245 1  |-  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ph  /\  ( ps  /\  ch  /\ 
th ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    /\ w3a 937    /\ w-bnj17 29052
This theorem is referenced by:  bnj290  29076  bnj563  29113  bnj919  29138  bnj976  29150  bnj543  29266  bnj570  29278  bnj594  29285  bnj916  29306  bnj917  29307  bnj964  29316  bnj983  29324  bnj984  29325  bnj998  29329  bnj999  29330  bnj1021  29337  bnj1083  29349  bnj1450  29421
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 179  df-an 362  df-3an 939  df-bnj17 29053
  Copyright terms: Public domain W3C validator