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 34717
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 34715 . 2 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)))
2 df-3an 1089 . . 3 ((𝜓𝜒𝜃) ↔ ((𝜓𝜒) ∧ 𝜃))
32anbi2i 623 . 2 ((𝜑 ∧ (𝜓𝜒𝜃)) ↔ (𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)))
41, 3bitr4i 278 1 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ (𝜓𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  w3a 1087  w-bnj17 34700
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 207  df-an 396  df-3an 1089  df-bnj17 34701
This theorem is referenced by:  bnj290  34724  bnj563  34757  bnj919  34781  bnj976  34791  bnj543  34907  bnj570  34919  bnj594  34926  bnj916  34947  bnj917  34948  bnj964  34957  bnj983  34965  bnj984  34966  bnj998  34971  bnj999  34972  bnj1021  34980  bnj1083  34992  bnj1450  35064
  Copyright terms: Public domain W3C validator