Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rp-fakeanorass Structured version   Unicode version

Theorem rp-fakeanorass 36064
 Description: A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by Richard Penner, 26-Feb-2020.)
Assertion
Ref Expression
rp-fakeanorass

Proof of Theorem rp-fakeanorass
StepHypRef Expression
1 pm1.4 387 . . . . . . . 8
21ord 378 . . . . . . 7
3 pm4.83 937 . . . . . . . 8
43biimpi 197 . . . . . . 7
52, 4sylan2 476 . . . . . 6
65ex 435 . . . . 5
76anim1d 566 . . . 4
8 orc 386 . . . . 5
98anim1i 570 . . . 4
107, 9jctir 540 . . 3
11 olc 385 . . . . . 6
12 olc 385 . . . . . 6
1311, 12jca 534 . . . . 5
14 simpl 458 . . . . 5
1513, 14imim12i 59 . . . 4
1710, 16impbii 190 . 2
18 dfbi2 632 . 2
19 ordir 873 . . . 4
2019bicomi 205 . . 3
2120bibi1i 315 . 2
2217, 18, 213bitr2i 276 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   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-or 371  df-an 372 This theorem is referenced by:  rp-fakeoranass  36065  rp-fakeinunass  36067
 Copyright terms: Public domain W3C validator