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

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

Proof of Theorem 3anan12
StepHypRef Expression
1 3anass 1089 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12 641 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitri 276 1 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  w3a 1081
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 1083
This theorem is referenced by:  3ancoma  1092  an33rean  1476  2reu5lem3  3752  snopeqop  5393  dff1o2  6617  ixxun  12744  elfz1b  12966  mreexexlem4d  16908  unocv  20740  iunocv  20741  iscvsp  23647  mbfmax  24165  ulm2  24888  iswwlks  27528  wwlksnfi  27598  wwlksnfiOLD  27599  eclclwwlkn1  27768  clwwlknon2x  27796  bnj548  32055  pridlnr  35182  brres2  35397  xrninxp  35507  sineq0ALT  41136  elbigo  44443
  Copyright terms: Public domain W3C validator