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 ⊢ φ ↔ ψ ∧ χ ↔ θ ∧ τ ↔ η → φ ∨ χ ∨ τ ↔ ψ ∨ θ ∨ η