Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  anddi2 Unicode version

Theorem anddi2 24941
Description: Conjunction of triple disjunctions. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Assertion
Ref Expression
anddi2  |-  ( ( ( ph  \/  ps  \/  ch )  /\  ( th  \/  ta  \/  et ) )  <->  ( (
( ph  /\  th )  \/  ( ph  /\  ta )  \/  ( ph  /\  et ) )  \/  ( ( ps  /\  th )  \/  ( ps 
/\  ta )  \/  ( ps  /\  et ) )  \/  ( ( ch 
/\  th )  \/  ( ch  /\  ta )  \/  ( ch  /\  et ) ) ) )

Proof of Theorem anddi2
StepHypRef Expression
1 df-3or 935 . . 3  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
2 df-3or 935 . . 3  |-  ( ( th  \/  ta  \/  et )  <->  ( ( th  \/  ta )  \/  et ) )
31, 2anbi12i 678 . 2  |-  ( ( ( ph  \/  ps  \/  ch )  /\  ( th  \/  ta  \/  et ) )  <->  ( (
( ph  \/  ps )  \/  ch )  /\  ( ( th  \/  ta )  \/  et ) ) )
4 andir 838 . 2  |-  ( ( ( ( ph  \/  ps )  \/  ch )  /\  ( ( th  \/  ta )  \/  et ) )  <->  ( (
( ph  \/  ps )  /\  ( ( th  \/  ta )  \/  et ) )  \/  ( ch  /\  (
( th  \/  ta )  \/  et )
) ) )
5 andir 838 . . . 4  |-  ( ( ( ph  \/  ps )  /\  ( ( th  \/  ta )  \/  et ) )  <->  ( ( ph  /\  ( ( th  \/  ta )  \/  et ) )  \/  ( ps  /\  (
( th  \/  ta )  \/  et )
) ) )
65orbi1i 506 . . 3  |-  ( ( ( ( ph  \/  ps )  /\  (
( th  \/  ta )  \/  et )
)  \/  ( ch 
/\  ( ( th  \/  ta )  \/  et ) ) )  <-> 
( ( ( ph  /\  ( ( th  \/  ta )  \/  et ) )  \/  ( ps  /\  ( ( th  \/  ta )  \/  et ) ) )  \/  ( ch  /\  ( ( th  \/  ta )  \/  et ) ) ) )
7 andi 837 . . . . 5  |-  ( (
ph  /\  ( ( th  \/  ta )  \/  et ) )  <->  ( ( ph  /\  ( th  \/  ta ) )  \/  ( ph  /\  et ) ) )
8 andi 837 . . . . 5  |-  ( ( ps  /\  ( ( th  \/  ta )  \/  et ) )  <->  ( ( ps  /\  ( th  \/  ta ) )  \/  ( ps  /\  et ) ) )
97, 8orbi12i 507 . . . 4  |-  ( ( ( ph  /\  (
( th  \/  ta )  \/  et )
)  \/  ( ps 
/\  ( ( th  \/  ta )  \/  et ) ) )  <-> 
( ( ( ph  /\  ( th  \/  ta ) )  \/  ( ph  /\  et ) )  \/  ( ( ps 
/\  ( th  \/  ta ) )  \/  ( ps  /\  et ) ) ) )
10 andi 837 . . . 4  |-  ( ( ch  /\  ( ( th  \/  ta )  \/  et ) )  <->  ( ( ch  /\  ( th  \/  ta ) )  \/  ( ch  /\  et ) ) )
119, 10orbi12i 507 . . 3  |-  ( ( ( ( ph  /\  ( ( th  \/  ta )  \/  et ) )  \/  ( ps  /\  ( ( th  \/  ta )  \/  et ) ) )  \/  ( ch  /\  ( ( th  \/  ta )  \/  et ) ) )  <->  ( (
( ( ph  /\  ( th  \/  ta )
)  \/  ( ph  /\  et ) )  \/  ( ( ps  /\  ( th  \/  ta )
)  \/  ( ps 
/\  et ) ) )  \/  ( ( ch  /\  ( th  \/  ta ) )  \/  ( ch  /\  et ) ) ) )
12 df-3or 935 . . . 4  |-  ( ( ( ( ( ph  /\ 
th )  \/  ( ph  /\  ta ) )  \/  ( ph  /\  et ) )  \/  (
( ( ps  /\  th )  \/  ( ps 
/\  ta ) )  \/  ( ps  /\  et ) )  \/  (
( ( ch  /\  th )  \/  ( ch 
/\  ta ) )  \/  ( ch  /\  et ) ) )  <->  ( (
( ( ( ph  /\ 
th )  \/  ( ph  /\  ta ) )  \/  ( ph  /\  et ) )  \/  (
( ( ps  /\  th )  \/  ( ps 
/\  ta ) )  \/  ( ps  /\  et ) ) )  \/  ( ( ( ch 
/\  th )  \/  ( ch  /\  ta ) )  \/  ( ch  /\  et ) ) ) )
13 df-3or 935 . . . . 5  |-  ( ( ( ph  /\  th )  \/  ( ph  /\ 
ta )  \/  ( ph  /\  et ) )  <-> 
( ( ( ph  /\ 
th )  \/  ( ph  /\  ta ) )  \/  ( ph  /\  et ) ) )
14 df-3or 935 . . . . 5  |-  ( ( ( ps  /\  th )  \/  ( ps  /\ 
ta )  \/  ( ps  /\  et ) )  <-> 
( ( ( ps 
/\  th )  \/  ( ps  /\  ta ) )  \/  ( ps  /\  et ) ) )
15 df-3or 935 . . . . 5  |-  ( ( ( ch  /\  th )  \/  ( ch  /\ 
ta )  \/  ( ch  /\  et ) )  <-> 
( ( ( ch 
/\  th )  \/  ( ch  /\  ta ) )  \/  ( ch  /\  et ) ) )
1613, 14, 153orbi123i 1141 . . . 4  |-  ( ( ( ( ph  /\  th )  \/  ( ph  /\ 
ta )  \/  ( ph  /\  et ) )  \/  ( ( ps 
/\  th )  \/  ( ps  /\  ta )  \/  ( ps  /\  et ) )  \/  (
( ch  /\  th )  \/  ( ch  /\ 
ta )  \/  ( ch  /\  et ) ) )  <->  ( ( ( ( ph  /\  th )  \/  ( ph  /\ 
ta ) )  \/  ( ph  /\  et ) )  \/  (
( ( ps  /\  th )  \/  ( ps 
/\  ta ) )  \/  ( ps  /\  et ) )  \/  (
( ( ch  /\  th )  \/  ( ch 
/\  ta ) )  \/  ( ch  /\  et ) ) ) )
17 andi 837 . . . . . . 7  |-  ( (
ph  /\  ( th  \/  ta ) )  <->  ( ( ph  /\  th )  \/  ( ph  /\  ta ) ) )
1817orbi1i 506 . . . . . 6  |-  ( ( ( ph  /\  ( th  \/  ta ) )  \/  ( ph  /\  et ) )  <->  ( (
( ph  /\  th )  \/  ( ph  /\  ta ) )  \/  ( ph  /\  et ) ) )
19 andi 837 . . . . . . 7  |-  ( ( ps  /\  ( th  \/  ta ) )  <-> 
( ( ps  /\  th )  \/  ( ps 
/\  ta ) ) )
2019orbi1i 506 . . . . . 6  |-  ( ( ( ps  /\  ( th  \/  ta ) )  \/  ( ps  /\  et ) )  <->  ( (
( ps  /\  th )  \/  ( ps  /\ 
ta ) )  \/  ( ps  /\  et ) ) )
2118, 20orbi12i 507 . . . . 5  |-  ( ( ( ( ph  /\  ( th  \/  ta )
)  \/  ( ph  /\  et ) )  \/  ( ( ps  /\  ( th  \/  ta )
)  \/  ( ps 
/\  et ) ) )  <->  ( ( ( ( ph  /\  th )  \/  ( ph  /\ 
ta ) )  \/  ( ph  /\  et ) )  \/  (
( ( ps  /\  th )  \/  ( ps 
/\  ta ) )  \/  ( ps  /\  et ) ) ) )
22 andi 837 . . . . . 6  |-  ( ( ch  /\  ( th  \/  ta ) )  <-> 
( ( ch  /\  th )  \/  ( ch 
/\  ta ) ) )
2322orbi1i 506 . . . . 5  |-  ( ( ( ch  /\  ( th  \/  ta ) )  \/  ( ch  /\  et ) )  <->  ( (
( ch  /\  th )  \/  ( ch  /\ 
ta ) )  \/  ( ch  /\  et ) ) )
2421, 23orbi12i 507 . . . 4  |-  ( ( ( ( ( ph  /\  ( th  \/  ta ) )  \/  ( ph  /\  et ) )  \/  ( ( ps 
/\  ( th  \/  ta ) )  \/  ( ps  /\  et ) ) )  \/  ( ( ch  /\  ( th  \/  ta ) )  \/  ( ch  /\  et ) ) )  <->  ( (
( ( ( ph  /\ 
th )  \/  ( ph  /\  ta ) )  \/  ( ph  /\  et ) )  \/  (
( ( ps  /\  th )  \/  ( ps 
/\  ta ) )  \/  ( ps  /\  et ) ) )  \/  ( ( ( ch 
/\  th )  \/  ( ch  /\  ta ) )  \/  ( ch  /\  et ) ) ) )
2512, 16, 243bitr4ri 269 . . 3  |-  ( ( ( ( ( ph  /\  ( th  \/  ta ) )  \/  ( ph  /\  et ) )  \/  ( ( ps 
/\  ( th  \/  ta ) )  \/  ( ps  /\  et ) ) )  \/  ( ( ch  /\  ( th  \/  ta ) )  \/  ( ch  /\  et ) ) )  <->  ( (
( ph  /\  th )  \/  ( ph  /\  ta )  \/  ( ph  /\  et ) )  \/  ( ( ps  /\  th )  \/  ( ps 
/\  ta )  \/  ( ps  /\  et ) )  \/  ( ( ch 
/\  th )  \/  ( ch  /\  ta )  \/  ( ch  /\  et ) ) ) )
266, 11, 253bitri 262 . 2  |-  ( ( ( ( ph  \/  ps )  /\  (
( th  \/  ta )  \/  et )
)  \/  ( ch 
/\  ( ( th  \/  ta )  \/  et ) ) )  <-> 
( ( ( ph  /\ 
th )  \/  ( ph  /\  ta )  \/  ( ph  /\  et ) )  \/  (
( ps  /\  th )  \/  ( ps  /\ 
ta )  \/  ( ps  /\  et ) )  \/  ( ( ch 
/\  th )  \/  ( ch  /\  ta )  \/  ( ch  /\  et ) ) ) )
273, 4, 263bitri 262 1  |-  ( ( ( ph  \/  ps  \/  ch )  /\  ( th  \/  ta  \/  et ) )  <->  ( (
( ph  /\  th )  \/  ( ph  /\  ta )  \/  ( ph  /\  et ) )  \/  ( ( ps  /\  th )  \/  ( ps 
/\  ta )  \/  ( ps  /\  et ) )  \/  ( ( ch 
/\  th )  \/  ( ch  /\  ta )  \/  ( ch  /\  et ) ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    /\ wa 358    \/ w3o 933
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935
  Copyright terms: Public domain W3C validator