Description: Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | astbstanbst.1 | |- ( ph <-> T. ) |
|
astbstanbst.2 | |- ( ps <-> T. ) |
||
Assertion | astbstanbst | |- ( ( ph /\ ps ) <-> T. ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | astbstanbst.1 | |- ( ph <-> T. ) |
|
2 | astbstanbst.2 | |- ( ps <-> T. ) |
|
3 | 1 | aistia | |- ph |
4 | 2 | aistia | |- ps |
5 | 3 4 | pm3.2i | |- ( ph /\ ps ) |
6 | 5 | bitru | |- ( ( ph /\ ps ) <-> T. ) |