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

Theorem uunT1 31865
Description: A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) Proof was revised to accomodate a possible future version of df-tru 1373. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
uunT1.1  |-  ( ( T.  /\  ph )  ->  ps )
Assertion
Ref Expression
uunT1  |-  ( ph  ->  ps )

Proof of Theorem uunT1
StepHypRef Expression
1 orc 385 . . 3  |-  ( ph  ->  ( ph  \/  -.  ph ) )
2 tru 1374 . . . . 5  |- T.
3 biid 236 . . . . 5  |-  ( ph  <->  ph )
42, 32th 239 . . . 4  |-  ( T.  <-> 
( ph  <->  ph ) )
5 exmid 415 . . . . . 6  |-  ( ph  \/  -.  ph )
65a1i 11 . . . . 5  |-  ( (
ph 
<-> 
ph )  ->  ( ph  \/  -.  ph )
)
7 biidd 237 . . . . 5  |-  ( (
ph  \/  -.  ph )  ->  ( ph  <->  ph ) )
86, 7impbii 188 . . . 4  |-  ( (
ph 
<-> 
ph )  <->  ( ph  \/  -.  ph ) )
94, 8bitri 249 . . 3  |-  ( T.  <-> 
( ph  \/  -.  ph ) )
101, 9sylibr 212 . 2  |-  ( ph  -> T.  )
11 uunT1.1 . 2  |-  ( ( T.  /\  ph )  ->  ps )
1210, 11mpancom 669 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369   T. wtru 1371
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-or 370  df-an 371  df-tru 1373
This theorem is referenced by:  uunT21  31867  sspwimpALT  32013
  Copyright terms: Public domain W3C validator