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

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

Proof of Theorem 3anan12
StepHypRef Expression
1 3anass 1109 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12 627 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitri 266 1 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  3ancoma  1112  an33rean  1600  2reu5lem3  3613  snopeqop  5160  snopeqopOLD  5161  dff1o2  6358  ixxun  12409  elfz1b  12632  mreexexlem4d  16512  unocv  20234  iunocv  20235  iscvsp  23140  mbfmax  23630  ulm2  24353  iswwlks  26957  wwlksnfi  27043  eclclwwlkn1  27226  clwwlknon2x  27271  bnj548  31290  pridlnr  34146  brres2  34352  xrninxp  34463  sineq0ALT  39667  elbigo  42913
  Copyright terms: Public domain W3C validator