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

Theorem 3anan32 1118
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 1109 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32 636 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
31, 2bitri 266 1 ((𝜑𝜓𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  3ancomb  1121  anandi3r  1128  rabssrabd  3849  dff1o3  6326  bropfvvvvlem  7458  tz7.49c  7745  ispos2  17214  lbsacsbs  19430  obslbs  20350  islbs4  20447  leordtvallem1  21294  trfbas2  21926  isclmp  23175  lssbn  23429  sineq0  24565  dchrelbas3  25254  nb3grpr2  26564  uspgr2wlkeq  26833  2spthd  27164  clwwlknonwwlknonb  27379  clwwlknonwwlknonbOLD  27380  frgr2wwlkeu  27607  elicoelioo  29989  cndprobprob  30948  bnj543  31411  elno3  32252  ellimits  32461  refsymrel2  34742  refsymrel3  34743  dfeqvrel2  34763  dfeqvrel3  34764
  Copyright terms: Public domain W3C validator