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

Theorem bnj252 33714
Description: -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
bnj252 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ (𝜓𝜒𝜃)))

Proof of Theorem bnj252
StepHypRef Expression
1 bnj250 33712 . 2 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)))
2 df-3an 1090 . . 3 ((𝜓𝜒𝜃) ↔ ((𝜓𝜒) ∧ 𝜃))
32anbi2i 624 . 2 ((𝜑 ∧ (𝜓𝜒𝜃)) ↔ (𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)))
41, 3bitr4i 278 1 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ (𝜓𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  w3a 1088  w-bnj17 33697
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 206  df-an 398  df-3an 1090  df-bnj17 33698
This theorem is referenced by:  bnj290  33721  bnj563  33754  bnj919  33778  bnj976  33788  bnj543  33904  bnj570  33916  bnj594  33923  bnj916  33944  bnj917  33945  bnj964  33954  bnj983  33962  bnj984  33963  bnj998  33968  bnj999  33969  bnj1021  33977  bnj1083  33989  bnj1450  34061
  Copyright terms: Public domain W3C validator