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 
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) )

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ).
2 simp1 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ph <-> ps ) )
3 1 2 e1a 
 |-  (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ph <-> ps ) ).
4 simp2 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ch <-> th ) )
5 1 4 e1a 
 |-  (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ch <-> th ) ).
6 pm4.39 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ( ph \/ ch ) <-> ( ps \/ th ) ) )
7 6 ex 
 |-  ( ( ph <-> ps ) -> ( ( ch <-> th ) -> ( ( ph \/ ch ) <-> ( ps \/ th ) ) ) )
8 3 5 7 e11 
 |-  (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch ) <-> ( ps \/ th ) ) ).
9 simp3 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ta <-> et ) )
10 1 9 e1a 
 |-  (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ta <-> et ) ).
11 pm4.39 
 |-  ( ( ( ( ph \/ ch ) <-> ( ps \/ th ) ) /\ ( ta <-> et ) ) -> ( ( ( ph \/ ch ) \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) )
12 11 ex 
 |-  ( ( ( ph \/ ch ) <-> ( ps \/ th ) ) -> ( ( ta <-> et ) -> ( ( ( ph \/ ch ) \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ) )
13 8 10 12 e11 
 |-  (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ( ph \/ ch ) \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ).
14 df-3or 
 |-  ( ( ph \/ ch \/ ta ) <-> ( ( ph \/ ch ) \/ ta ) )
15 14 bicomi 
 |-  ( ( ( ph \/ ch ) \/ ta ) <-> ( ph \/ ch \/ ta ) )
16 bitr3 
 |-  ( ( ( ( ph \/ ch ) \/ ta ) <-> ( ph \/ ch \/ ta ) ) -> ( ( ( ( ph \/ ch ) \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) -> ( ( ph \/ ch \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ) )
17 16 com12 
 |-  ( ( ( ( ph \/ ch ) \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) -> ( ( ( ( ph \/ ch ) \/ ta ) <-> ( ph \/ ch \/ ta ) ) -> ( ( ph \/ ch \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ) )
18 13 15 17 e10 
 |-  (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ).
19 df-3or 
 |-  ( ( ps \/ th \/ et ) <-> ( ( ps \/ th ) \/ et ) )
20 19 bicomi 
 |-  ( ( ( ps \/ th ) \/ et ) <-> ( ps \/ th \/ et ) )
21 bitr 
 |-  ( ( ( ( ph \/ ch \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) /\ ( ( ( ps \/ th ) \/ et ) <-> ( ps \/ th \/ et ) ) ) -> ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) )
22 21 ex 
 |-  ( ( ( ph \/ ch \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) -> ( ( ( ( ps \/ th ) \/ et ) <-> ( ps \/ th \/ et ) ) -> ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) ) )
23 18 20 22 e10 
 |-  (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) ).
24 23 in1 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) -> ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) ) )