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

Theorem 3anan12 1049
 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 1043 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
2 3anass 1040 . 2 ((𝜓𝜑𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitri 264 1 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 384   ∧ w3a 1036 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 386  df-3an 1038 This theorem is referenced by:  an33rean  1443  2reu5lem3  3402  snopeqop  4939  fncnv  5930  dff1o2  6109  ixxun  12149  mreexexlem4d  16247  unocv  19964  iunocv  19965  iscvsp  22868  mbfmax  23356  ulm2  24077  iswwlks  26631  wwlksnfi  26704  eclclwwlksn1  26852  numclwlk1lem2f1  27116  bnj548  30728  pridlnr  33506  sineq0ALT  38695  elbigo  41667
 Copyright terms: Public domain W3C validator