Theorem 3ancomb 1047

Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
3ancomb	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Proof of Theorem 3ancomb

Step	Hyp	Ref	Expression
1		3ancoma 1045	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3anrot 1043	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))
3	1, 2	bitri 264	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))

Syntax hints:   ↔ wb 196   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3simpb  1059  an33rean  1446  elioore  12205  leexp2  12915  swrdswrd  13460  pcgcd  15582  ablsubsub23  18230  xmetrtri  22160  phtpcer  22794  phtpcerOLD  22795  ishl2  23166  rusgrprc  26486  numclwwlkovf2num  27218  ablo32  27403  ablodivdiv  27407  ablodiv32  27409  bnj268  30775  bnj945  30844  bnj944  31008  bnj969  31016  btwncom  32121  btwnswapid2  32125  btwnouttr  32131  cgr3permute1  32155  colinearperm1  32169  endofsegid  32192  colinbtwnle  32225  broutsideof2  32229  outsideofcom  32235  neificl  33549  lhpexle2  35296  uunTT1p1  39021  uun123  39035  smflimlem4  40982  alsi-no-surprise  42542