Metamath Proof Explorer


Theorem 3orbi123VD

Description: Virtual deduction proof of 3orbi123 . 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 ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ).
2:1,?: e1a |- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ph <-> ps ) ).
3:1,?: e1a |- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ch <-> th ) ).
4:1,?: e1a |- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ta <-> et ) ).
5:2,3,?: e11 |- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch ) <-> ( ps \/ th ) ) ).
6:5,4,?: e11 |- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ( ph \/ ch ) \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ).
7:?: |- ( ( ( ph \/ ch ) \/ ta ) <-> ( ph \/ ch \/ ta ) )
8:6,7,?: e10 |- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ).
9:?: |- ( ( ( ps \/ th ) \/ et ) <-> ( ps \/ th \/ et ) )
10:8,9,?: e10 |- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) ).
qed:10: |- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) )
(Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 3orbi123VD φψχθτηφχτψθη

Proof

Step Hyp Ref Expression
1 idn1 φψχθτηφψχθτη
2 simp1 φψχθτηφψ
3 1 2 e1a φψχθτηφψ
4 simp2 φψχθτηχθ
5 1 4 e1a φψχθτηχθ
6 pm4.39 φψχθφχψθ
7 6 ex φψχθφχψθ
8 3 5 7 e11 φψχθτηφχψθ
9 simp3 φψχθτητη
10 1 9 e1a φψχθτητη
11 pm4.39 φχψθτηφχτψθη
12 11 ex φχψθτηφχτψθη
13 8 10 12 e11 φψχθτηφχτψθη
14 df-3or φχτφχτ
15 14 bicomi φχτφχτ
16 bitr3 φχτφχτφχτψθηφχτψθη
17 16 com12 φχτψθηφχτφχτφχτψθη
18 13 15 17 e10 φψχθτηφχτψθη
19 df-3or ψθηψθη
20 19 bicomi ψθηψθη
21 bitr φχτψθηψθηψθηφχτψθη
22 21 ex φχτψθηψθηψθηφχτψθη
23 18 20 22 e10 φψχθτηφχτψθη
24 23 in1 φψχθτηφχτψθη