Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  uun2221p1 Structured version   Unicode version

Theorem uun2221p1 31902
 Description: A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
uun2221p1.1
Assertion
Ref Expression
uun2221p1

Proof of Theorem uun2221p1
StepHypRef Expression
1 uun2221p1.1 . . 3
2 3anrot 970 . . . 4
32imbi1i 325 . . 3
41, 3mpbir 209 . 2
5 3anass 969 . . . . . 6
6 anabs5 807 . . . . . 6
75, 6bitri 249 . . . . 5
8 ancom 450 . . . . . 6
98anbi2i 694 . . . . 5
107, 9bitr4i 252 . . . 4
11 anabs5 807 . . . . 5
1211, 8bitri 249 . . . 4
1310, 12bitri 249 . . 3
1413imbi1i 325 . 2
154, 14mpbi 208 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 965 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 185  df-an 371  df-3an 967 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator