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 29510
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 29508 . 2  |-  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ph  /\  ( ( ps  /\  ch )  /\  th )
) )
2 df-3an 985 . . 3  |-  ( ( ps  /\  ch  /\  th )  <->  ( ( ps 
/\  ch )  /\  th ) )
32anbi2i 699 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  <->  ( ph  /\  ( ( ps  /\  ch )  /\  th )
) )
41, 3bitr4i 256 1  |-  ( (
ph  /\  ps  /\  ch  /\ 
th )  <->  ( ph  /\  ( ps  /\  ch  /\ 
th ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371    /\ w3a 983    /\ w-bnj17 29493
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 189  df-an 373  df-3an 985  df-bnj17 29494
This theorem is referenced by:  bnj290  29517  bnj563  29555  bnj919  29580  bnj976  29591  bnj543  29706  bnj570  29718  bnj594  29725  bnj916  29746  bnj917  29747  bnj964  29756  bnj983  29764  bnj984  29765  bnj998  29769  bnj999  29770  bnj1021  29777  bnj1083  29789  bnj1450  29861
  Copyright terms: Public domain W3C validator