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

Theorem 3anan12 1044
 Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
3anan12 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))

Proof of Theorem 3anan12
StepHypRef Expression
1 3ancoma 1038 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
2 3anass 1035 . 2 ((𝜓𝜑𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitri 263 1 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  an33rean  1438  2reu5lem3  3382  snopeqop  4894  fncnv  5876  dff1o2  6055  ixxun  12062  mreexexlem4d  16130  unocv  19843  iunocv  19844  iscvsp  22736  mbfmax  23222  ulm2  23943  usgra2wlkspthlem2  26148  wwlknprop  26214  wwlknfi  26266  eclclwwlkn1  26359  numclwwlkovf2  26611  numclwlk1lem2f1  26621  bnj548  30221  pridlnr  33005  sineq0ALT  38195  iswwlks  41039  wwlksnfi  41112  eclclwwlksn1  41259  av-numclwlk1lem2f1  41524  elbigo  42143
 Copyright terms: Public domain W3C validator