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