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

Theorem 3anan32 1094
 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 1086 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32 645 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
31, 2bitri 278 1 ((𝜑𝜓𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  3ancomb  1096  anandi3r  1100  rabssrabd  4033  dff1o3  6603  bropfvvvvlem  7773  tz7.49c  8069  ispos2  17549  lbsacsbs  19919  obslbs  20417  islbs4  20519  leordtvallem1  21813  trfbas2  22446  isclmp  23700  lssbn  23954  sineq0  25114  dchrelbas3  25820  nb3grpr2  27171  uspgr2wlkeq  27433  2spthd  27725  clwwlknonwwlknonb  27889  frgr2wwlkeu  28110  elicoelioo  30511  cndprobprob  31770  bnj543  32239  cusgr3cyclex  32457  elno3  33236  ellimits  33445  refsymrel2  35921  refsymrel3  35922  dfeqvrel2  35943  dfeqvrel3  35944
 Copyright terms: Public domain W3C validator