Mathbox for Rodolfo Medina < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prtlem70 Structured version   Unicode version

Theorem prtlem70 26652
 Description: Lemma for prter3 26685: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)
Assertion
Ref Expression
prtlem70

Proof of Theorem prtlem70
StepHypRef Expression
1 anass 631 . . . 4
21anbi1i 677 . . 3
3 anandi 802 . . . . 5
43anbi1i 677 . . . 4
54anbi1i 677 . . 3
6 anass 631 . . . . 5
7 anass 631 . . . . . 6
87anbi1i 677 . . . . 5
9 ancom 438 . . . . 5
106, 8, 93bitr4ri 270 . . . 4
11 ancom 438 . . . . 5
1211anbi1i 677 . . . 4
13 anass 631 . . . . 5
14 ancom 438 . . . . 5
1513, 14bitri 241 . . . 4
1610, 12, 153bitri 263 . . 3
172, 5, 163bitr4ri 270 . 2
18 anass 631 . . 3
1918anbi1i 677 . 2
20 an4 798 . . . . 5
21 anass 631 . . . . 5
2220, 21bitri 241 . . . 4
2322anbi2i 676 . . 3
2423anbi1i 677 . 2
2517, 19, 243bitri 263 1
 Colors of variables: wff set class Syntax hints:   wb 177   wa 359 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 178  df-an 361
 Copyright terms: Public domain W3C validator