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  1484  2reu5lem3  3762  snopeqop  5510  dff1o2  6852  ixxun  13404  elfz1b  13634  mreexexlem4d  17691  unocv  21699  iunocv  21700  iscvsp  25162  mbfmax  25685  ulm2  26429  iswwlks  29857  wwlksnfi  29927  eclclwwlkn1  30095  clwwlknon2x  30123  bnj548  34912  pridlnr  38044  brres2  38270  xrninxp  38394  sineq0ALT  44962  elbigo  48477
  Copyright terms: Public domain W3C validator