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

Theorem 3anan12 1093
 Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised to shorten 3ancoma 1095 by Wolf Lammen, 5-Jun-2022.)
Assertion
Ref Expression
3anan12 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))

Proof of Theorem 3anan12
StepHypRef Expression
1 3anass 1092 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12 644 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitri 278 1 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  3ancoma  1095  an33rean  1480  an33reanOLD  1481  2reu5lem3  3671  snopeqop  5365  dff1o2  6607  ixxun  12795  elfz1b  13025  mreexexlem4d  16976  unocv  20445  iunocv  20446  iscvsp  23829  mbfmax  24349  ulm2  25079  iswwlks  27721  wwlksnfi  27791  eclclwwlkn1  27959  clwwlknon2x  27987  bnj548  32397  pridlnr  35754  brres2  35969  xrninxp  36080  sineq0ALT  42016  elbigo  45330
 Copyright terms: Public domain W3C validator