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

Theorem 3anan32 1043
 Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Assertion
Ref Expression
3anan32 ((𝜑𝜓𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))

Proof of Theorem 3anan32
StepHypRef Expression
1 df-3an 1033 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 an32 835 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
31, 2bitri 263 1 ((𝜑𝜓𝜒) ↔ ((𝜑𝜒) ∧ 𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  anandi3r  1046  dff1o3  6056  bropfvvvvlem  7143  tz7.49c  7428  ispos2  16771  lbsacsbs  18977  obslbs  19893  islbs4  19990  leordtvallem1  20824  trfbas2  21457  isclmp  22705  lssbn  22956  sineq0  24077  dchrelbas3  24763  nb3grapr2  25983  usg2wlkeq  26236  elicoelioo  28930  cndprobprob  29827  bnj543  30217  elno3  31052  ellimits  31187  nb3grpr2  40611  uspgr2wlkeq  40854  2spthd  41148
 Copyright terms: Public domain W3C validator