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

Theorem 3anan32 1082
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 1073 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32 625 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
31, 2bitri 264 1 ((𝜑𝜓𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  3ancomb  1085  anandi3r  1092  rabssrabd  3838  dff1o3  6285  bropfvvvvlem  7411  tz7.49c  7698  ispos2  17156  lbsacsbs  19371  obslbs  20291  islbs4  20388  leordtvallem1  21235  trfbas2  21867  isclmp  23116  lssbn  23367  sineq0  24494  dchrelbas3  25184  nb3grpr2  26508  uspgr2wlkeq  26777  2spthd  27088  clwwlknonwwlknonb  27281  clwwlknonwwlknonbOLD  27282  frgr2wwlkeu  27509  elicoelioo  29880  cndprobprob  30840  bnj543  31301  elno3  32145  ellimits  32354  refsymrel2  34655  refsymrel3  34656
  Copyright terms: Public domain W3C validator