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

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

Proof of Theorem 3anan12
StepHypRef Expression
1 3anass 1094 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
2 an12 645 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitri 275 1 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  3ancoma  1097  an33rean  1482  2reu5lem3  3766  snopeqop  5516  dff1o2  6854  ixxun  13400  elfz1b  13630  mreexexlem4d  17692  unocv  21716  iunocv  21717  iscvsp  25175  mbfmax  25698  ulm2  26443  iswwlks  29866  wwlksnfi  29936  eclclwwlkn1  30104  clwwlknon2x  30132  bnj548  34890  pridlnr  38023  brres2  38250  xrninxp  38374  sineq0ALT  44935  elbigo  48401
  Copyright terms: Public domain W3C validator