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 31282
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 31280 . 2 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)))
2 df-3an 1110 . . 3 ((𝜓𝜒𝜃) ↔ ((𝜓𝜒) ∧ 𝜃))
32anbi2i 617 . 2 ((𝜑 ∧ (𝜓𝜒𝜃)) ↔ (𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)))
41, 3bitr4i 270 1 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ (𝜓𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 385  w3a 1108  w-bnj17 31265
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 199  df-an 386  df-3an 1110  df-bnj17 31266
This theorem is referenced by:  bnj290  31289  bnj563  31323  bnj919  31347  bnj976  31358  bnj543  31473  bnj570  31485  bnj594  31492  bnj916  31513  bnj917  31514  bnj964  31523  bnj983  31531  bnj984  31532  bnj998  31536  bnj999  31537  bnj1021  31544  bnj1083  31556  bnj1450  31628
  Copyright terms: Public domain W3C validator