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

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

Proof of Theorem 3anrev
StepHypRef Expression
1 3ancoma 1097 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
2 3anrot 1099 . 2 ((𝜒𝜓𝜑) ↔ (𝜓𝜑𝜒))
31, 2bitr4i 278 1 ((𝜑𝜓𝜒) ↔ (𝜒𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 206  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:  an33rean  1484  nnmcan  8673  odupos  18374  wwlks2onsym  29979  frgr3v  30295  bnj345  34729  bnj1098  34798  pocnv  35764  btwnswapid2  36020  colinbtwnle  36120  uunT11p2  44823  uunT12p5  44829  uun2221p2  44840  grtriproplem  47911  grtrif1o  47914
  Copyright terms: Public domain W3C validator