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 31861
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 31859 . 2 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)))
2 df-3an 1083 . . 3 ((𝜓𝜒𝜃) ↔ ((𝜓𝜒) ∧ 𝜃))
32anbi2i 622 . 2 ((𝜑 ∧ (𝜓𝜒𝜃)) ↔ (𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)))
41, 3bitr4i 279 1 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ (𝜓𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  w3a 1081  w-bnj17 31844
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 208  df-an 397  df-3an 1083  df-bnj17 31845
This theorem is referenced by:  bnj290  31868  bnj563  31902  bnj919  31926  bnj976  31937  bnj543  32053  bnj570  32065  bnj594  32072  bnj916  32093  bnj917  32094  bnj964  32103  bnj983  32111  bnj984  32112  bnj998  32116  bnj999  32117  bnj1021  32124  bnj1083  32136  bnj1450  32208
  Copyright terms: Public domain W3C validator