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

Theorem 3anan12 1082
 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 1084 by Wolf Lammen, 5-Jun-2022.)
Assertion
Ref Expression
3anan12 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))

Proof of Theorem 3anan12
StepHypRef Expression
1 3anass 1081 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12 873 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitri 264 1 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383   ∧ w3a 1072 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 385  df-3an 1074 This theorem is referenced by:  3ancoma  1084  an33rean  1595  2reu5lem3  3557  snopeqop  5118  fncnv  6124  dff1o2  6305  ixxun  12405  elfz1b  12623  mreexexlem4d  16530  unocv  20247  iunocv  20248  iscvsp  23149  mbfmax  23636  ulm2  24359  iswwlks  26961  wwlksnfi  27046  eclclwwlkn1  27228  clwwlknon2x  27273  bnj548  31296  pridlnr  34167  brres2  34378  xrninxp  34492  sineq0ALT  39691  elbigo  42874
 Copyright terms: Public domain W3C validator