MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anan32 Structured version   Visualization version   GIF version

Theorem 3anan32 1048
Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Assertion
Ref Expression
3anan32 ((𝜑𝜓𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))

Proof of Theorem 3anan32
StepHypRef Expression
1 df-3an 1038 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32 838 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
31, 2bitri 264 1 ((𝜑𝜓𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  anandi3r  1051  dff1o3  6100  bropfvvvvlem  7201  tz7.49c  7486  ispos2  16869  lbsacsbs  19075  obslbs  19993  islbs4  20090  leordtvallem1  20924  trfbas2  21557  isclmp  22805  lssbn  23056  sineq0  24177  dchrelbas3  24863  nb3grpr2  26172  uspgr2wlkeq  26411  2spthd  26706  elicoelioo  29381  cndprobprob  30278  bnj543  30668  elno3  31506  ellimits  31656
  Copyright terms: Public domain W3C validator