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

Theorem 3anan32 1089
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 1081 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32 642 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
31, 2bitri 276 1 ((𝜑𝜓𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  3ancomb  1091  anandi3r  1095  rabssrabd  4055  dff1o3  6614  bropfvvvvlem  7775  tz7.49c  8071  ispos2  17546  lbsacsbs  19857  obslbs  20802  islbs4  20904  leordtvallem1  21746  trfbas2  22379  isclmp  23628  lssbn  23882  sineq0  25036  dchrelbas3  25741  nb3grpr2  27092  uspgr2wlkeq  27354  2spthd  27647  clwwlknonwwlknonb  27812  frgr2wwlkeu  28033  elicoelioo  30427  cndprobprob  31595  bnj543  32064  cusgr3cyclex  32280  elno3  33059  ellimits  33268  refsymrel2  35683  refsymrel3  35684  dfeqvrel2  35705  dfeqvrel3  35706
  Copyright terms: Public domain W3C validator