Metamath Proof Explorer

Theorem orbi1rVD

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

Ref Expression
Assertion orbi1rVD ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜒 ∨ 𝜑 ) ↔ ( 𝜒 ∨ 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    ( 𝜑 ↔ 𝜓 )    ▶    ( 𝜑 ↔ 𝜓 )    )
2 idn2 ⊢ (    ( 𝜑 ↔ 𝜓 )    ,    ( 𝜒 ∨ 𝜑 )    ▶    ( 𝜒 ∨ 𝜑 )    )
3 pm1.4 ⊢ ( ( 𝜒 ∨ 𝜑 ) → ( 𝜑 ∨ 𝜒 ) )
4 2 3 e2 ⊢ (    ( 𝜑 ↔ 𝜓 )    ,    ( 𝜒 ∨ 𝜑 )    ▶    ( 𝜑 ∨ 𝜒 )    )
5 orbi1 ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ∨ 𝜒 ) ↔ ( 𝜓 ∨ 𝜒 ) ) )
6 5 biimpd ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ∨ 𝜒 ) → ( 𝜓 ∨ 𝜒 ) ) )
7 1 4 6 e12 ⊢ (    ( 𝜑 ↔ 𝜓 )    ,    ( 𝜒 ∨ 𝜑 )    ▶    ( 𝜓 ∨ 𝜒 )    )
8 pm1.4 ⊢ ( ( 𝜓 ∨ 𝜒 ) → ( 𝜒 ∨ 𝜓 ) )
9 7 8 e2 ⊢ (    ( 𝜑 ↔ 𝜓 )    ,    ( 𝜒 ∨ 𝜑 )    ▶    ( 𝜒 ∨ 𝜓 )    )
10 9 in2 ⊢ (    ( 𝜑 ↔ 𝜓 )    ▶    ( ( 𝜒 ∨ 𝜑 ) → ( 𝜒 ∨ 𝜓 ) )    )
11 idn2 ⊢ (    ( 𝜑 ↔ 𝜓 )    ,    ( 𝜒 ∨ 𝜓 )    ▶    ( 𝜒 ∨ 𝜓 )    )
12 pm1.4 ⊢ ( ( 𝜒 ∨ 𝜓 ) → ( 𝜓 ∨ 𝜒 ) )
13 11 12 e2 ⊢ (    ( 𝜑 ↔ 𝜓 )    ,    ( 𝜒 ∨ 𝜓 )    ▶    ( 𝜓 ∨ 𝜒 )    )
14 5 biimprd ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜓 ∨ 𝜒 ) → ( 𝜑 ∨ 𝜒 ) ) )
15 1 13 14 e12 ⊢ (    ( 𝜑 ↔ 𝜓 )    ,    ( 𝜒 ∨ 𝜓 )    ▶    ( 𝜑 ∨ 𝜒 )    )
16 pm1.4 ⊢ ( ( 𝜑 ∨ 𝜒 ) → ( 𝜒 ∨ 𝜑 ) )
17 15 16 e2 ⊢ (    ( 𝜑 ↔ 𝜓 )    ,    ( 𝜒 ∨ 𝜓 )    ▶    ( 𝜒 ∨ 𝜑 )    )
18 17 in2 ⊢ (    ( 𝜑 ↔ 𝜓 )    ▶    ( ( 𝜒 ∨ 𝜓 ) → ( 𝜒 ∨ 𝜑 ) )    )
19 impbi ⊢ ( ( ( 𝜒 ∨ 𝜑 ) → ( 𝜒 ∨ 𝜓 ) ) → ( ( ( 𝜒 ∨ 𝜓 ) → ( 𝜒 ∨ 𝜑 ) ) → ( ( 𝜒 ∨ 𝜑 ) ↔ ( 𝜒 ∨ 𝜓 ) ) ) )
20 10 18 19 e11 ⊢ (    ( 𝜑 ↔ 𝜓 )    ▶    ( ( 𝜒 ∨ 𝜑 ) ↔ ( 𝜒 ∨ 𝜓 ) )    )
21 20 in1 ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜒 ∨ 𝜑 ) ↔ ( 𝜒 ∨ 𝜓 ) ) )