Description: A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015) Proof was revised to accommodate a possible future version of df-tru . (Revised by David A. Wheeler, 8-May-2019) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | uunT1.1 | |- ( ( T. /\ ph ) -> ps ) |
|
| Assertion | uunT1 | |- ( ph -> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uunT1.1 | |- ( ( T. /\ ph ) -> ps ) |
|
| 2 | orc | |- ( ph -> ( ph \/ -. ph ) ) |
|
| 3 | tru | |- T. |
|
| 4 | biid | |- ( ph <-> ph ) |
|
| 5 | 3 4 | 2th | |- ( T. <-> ( ph <-> ph ) ) |
| 6 | exmid | |- ( ph \/ -. ph ) |
|
| 7 | 6 | a1i | |- ( ( ph <-> ph ) -> ( ph \/ -. ph ) ) |
| 8 | biidd | |- ( ( ph \/ -. ph ) -> ( ph <-> ph ) ) |
|
| 9 | 7 8 | impbii | |- ( ( ph <-> ph ) <-> ( ph \/ -. ph ) ) |
| 10 | 5 9 | bitri | |- ( T. <-> ( ph \/ -. ph ) ) |
| 11 | 2 10 | sylibr | |- ( ph -> T. ) |
| 12 | 11 1 | mpancom | |- ( ph -> ps ) |