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

Theorem 3ancomb 1045
Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3ancomb ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))

Proof of Theorem 3ancomb
StepHypRef Expression
1 3ancoma 1043 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
2 3anrot 1041 . 2 ((𝜓𝜑𝜒) ↔ (𝜑𝜒𝜓))
31, 2bitri 264 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  w3a 1036
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 1038
This theorem is referenced by:  3simpb  1057  an33rean  1443  elioore  12144  leexp2  12852  swrdswrd  13393  pcgcd  15501  ablsubsub23  18146  xmetrtri  22065  phtpcer  22697  phtpcerOLD  22698  ishl2  23069  rusgrprc  26350  numclwwlkovf2num  27068  ablo32  27243  ablodivdiv  27247  ablodiv32  27249  bnj268  30474  bnj945  30544  bnj944  30708  bnj969  30716  btwncom  31755  btwnswapid2  31759  btwnouttr  31765  cgr3permute1  31789  colinearperm1  31803  endofsegid  31826  colinbtwnle  31859  broutsideof2  31863  outsideofcom  31869  neificl  33167  lhpexle2  34762  uunTT1p1  38489  uun123  38503  smflimlem4  40276  alsi-no-surprise  41819
  Copyright terms: Public domain W3C validator