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  1482  nnmcan  8671  odupos  18386  wwlks2onsym  29988  frgr3v  30304  bnj345  34707  bnj1098  34776  pocnv  35743  btwnswapid2  36000  colinbtwnle  36100  uunT11p2  44796  uunT12p5  44802  uun2221p2  44813  grtriproplem  47844  grtrif1o  47847
  Copyright terms: Public domain W3C validator