Theorem bitr3VD 16673

Description: Virtual deduction proof of bitr3 1283. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- . (ph <-> ps)   ⊢   (ph <-> ps) .
2:1,?: e1_ 16518	|- . (ph <-> ps)   ⊢   (ps <-> ph) .
3::	|- . (ph <-> ps), (ph <-> ch)    ⊢   (ph <-> ch) .
4:3,?: e2 16521	|- . (ph <-> ps), (ph <-> ch)    ⊢   (ch <-> ph) .
5:2,4,?: e12 16593	|- . (ph <-> ps), (ph <-> ch)    ⊢   (ps <-> ch) .
6:5:	|- . (ph <-> ps)   ⊢   ((ph <-> ch) -> (ps <-> ch)) .
qed:6:	|- ((ph <-> ps) -> ((ph <-> ch) -> (ps <-> ch)))

Assertion

Ref	Expression
bitr3VD	|- ((ph <-> ps) -> ((ph <-> ch) -> (ps <-> ch)))

Proof of Theorem bitr3VD

Step	Hyp	Ref	Expression
1		idn1 16484	. . . . 5 |- . (ph <-> ps)   ⊢   (ph <-> ps) .
2		id 73	. . . . . 6 |- ((ph <-> ps) -> (ph <-> ps))
3	2	bicomd 580	. . . . 5 |- ((ph <-> ps) -> (ps <-> ph))
4	1, 3	e1_ 16518	. . . 4 |- . (ph <-> ps)   ⊢   (ps <-> ph) .
5		idn2 16509	. . . . 5 |- . (ph <-> ps), (ph <-> ch)   ⊢   (ph <-> ch) .
6		id 73	. . . . . 6 |- ((ph <-> ch) -> (ph <-> ch))
7	6	bicomd 580	. . . . 5 |- ((ph <-> ch) -> (ch <-> ph))
8	5, 7	e2 16521	. . . 4 |- . (ph <-> ps), (ph <-> ch)   ⊢   (ch <-> ph) .
9		biantr 814	. . . . 5 |- (((ps <-> ph) /\ (ch <-> ph)) -> (ps <-> ch))
10	9	ex 402	. . . 4 |- ((ps <-> ph) -> ((ch <-> ph) -> (ps <-> ch)))
11	4, 8, 10	e12 16593	. . 3 |- . (ph <-> ps), (ph <-> ch)   ⊢   (ps <-> ch) .
12	11	in2 16506	. 2 |- . (ph <-> ps)   ⊢   ((ph <-> ch) -> (ps <-> ch)) .
13	12	in1 16481	1 |- ((ph <-> ps) -> ((ph <-> ch) -> (ps <-> ch)))

Syntax hints:   -> wi 3   <-> wb 163

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-vd1 16480  df-vd2 16489

Copyright terms: Public domain