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 31070
 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 31068 . 2 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)))
2 df-3an 1074 . . 3 ((𝜓𝜒𝜃) ↔ ((𝜓𝜒) ∧ 𝜃))
32anbi2i 732 . 2 ((𝜑 ∧ (𝜓𝜒𝜃)) ↔ (𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)))
41, 3bitr4i 267 1 ((𝜑𝜓𝜒𝜃) ↔ (𝜑 ∧ (𝜓𝜒𝜃)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   ∧ w-bnj17 31053 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 197  df-an 385  df-3an 1074  df-bnj17 31054 This theorem is referenced by:  bnj290  31077  bnj563  31112  bnj919  31136  bnj976  31147  bnj543  31262  bnj570  31274  bnj594  31281  bnj916  31302  bnj917  31303  bnj964  31312  bnj983  31320  bnj984  31321  bnj998  31325  bnj999  31326  bnj1021  31333  bnj1083  31345  bnj1450  31417
 Copyright terms: Public domain W3C validator