MPE Home 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 643 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitri 274 1 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  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 206  df-an 395  df-3an 1086
This theorem is referenced by:  3ancoma  1095  an33rean  1480  2reu5lem3  3751  snopeqop  5512  dff1o2  6848  ixxun  13394  elfz1b  13624  mreexexlem4d  17660  unocv  21676  iunocv  21677  iscvsp  25146  mbfmax  25669  ulm2  26414  iswwlks  29770  wwlksnfi  29840  eclclwwlkn1  30008  clwwlknon2x  30036  bnj548  34742  pridlnr  37737  brres2  37966  xrninxp  38090  sineq0ALT  44613  elbigo  47939
  Copyright terms: Public domain W3C validator