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 ⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜃 ) ∧ ( 𝜏 ↔ 𝜂 ) ) → ( ( 𝜑 ∨ 𝜒 ∨ 𝜏 ) ↔ ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ) )