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

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

Proof of Theorem prtlem70
StepHypRef Expression
1 anass 653 . . . 4
21anbi1i 699 . . 3
3 anandi 835 . . . . 5
43anbi1i 699 . . . 4
54anbi1i 699 . . 3
6 anass 653 . . . . 5
7 anass 653 . . . . . 6
87anbi1i 699 . . . . 5
9 ancom 451 . . . . 5
106, 8, 93bitr4ri 281 . . . 4
11 ancom 451 . . . . 5
1211anbi1i 699 . . . 4
13 anass 653 . . . . 5
14 ancom 451 . . . . 5
1513, 14bitri 252 . . . 4
1610, 12, 153bitri 274 . . 3
172, 5, 163bitr4ri 281 . 2
18 anass 653 . . 3
1918anbi1i 699 . 2
20 an4 831 . . . . 5
21 anass 653 . . . . 5
2220, 21bitri 252 . . . 4
2322anbi2i 698 . . 3
2423anbi1i 699 . 2
2517, 19, 243bitri 274 1
 Colors of variables: wff setvar class Syntax hints:   wb 187   wa 370 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 188  df-an 372 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator