Description: Virtual deduction proof of 3ornot23 . 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 \/ ps ) ->. ( ch \/ ph \/ ps ) ). |
| 3:1,?: e1a | |- (. ( -. ph /\ -. ps ) ->. -. ph ). |
| 4:1,?: e1a | |- (. ( -. ph /\ -. ps ) ->. -. ps ). |
| 5:3,4,?: e11 | |- (. ( -. ph /\ -. ps ) ->. -. ( ph \/ ps ) ). |
| 6:2,?: e2 | |- (. ( -. ph /\ -. ps ) ,. ( ch \/ ph \/ ps ) ->. ( ch \/ ( ph \/ ps ) ) ). |
| 7:5,6,?: e12 | |- (. ( -. ph /\ -. ps ) ,. ( ch \/ ph \/ ps ) ->. ch ). |
| 8:7: | |- (. ( -. ph /\ -. ps ) ->. ( ( ch \/ ph \/ ps ) -> ch ) ). |
| qed:8: | |- ( ( -. ph /\ -. ps ) -> ( ( ch \/ ph \/ ps ) -> ch ) ) |
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 3ornot23VD | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → ( ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) → 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | idn1 | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) ▶ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) | |
| 2 | simpl | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → ¬ 𝜑 ) | |
| 3 | 1 2 | e1a | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) ▶ ¬ 𝜑 ) |
| 4 | simpr | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → ¬ 𝜓 ) | |
| 5 | 1 4 | e1a | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) ▶ ¬ 𝜓 ) |
| 6 | ioran | ⊢ ( ¬ ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) | |
| 7 | 6 | simplbi2 | ⊢ ( ¬ 𝜑 → ( ¬ 𝜓 → ¬ ( 𝜑 ∨ 𝜓 ) ) ) |
| 8 | 3 5 7 | e11 | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) ▶ ¬ ( 𝜑 ∨ 𝜓 ) ) |
| 9 | idn2 | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) , ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) ▶ ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) ) | |
| 10 | 3orass | ⊢ ( ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) ↔ ( 𝜒 ∨ ( 𝜑 ∨ 𝜓 ) ) ) | |
| 11 | 10 | biimpi | ⊢ ( ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) → ( 𝜒 ∨ ( 𝜑 ∨ 𝜓 ) ) ) |
| 12 | 9 11 | e2 | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) , ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) ▶ ( 𝜒 ∨ ( 𝜑 ∨ 𝜓 ) ) ) |
| 13 | orel2 | ⊢ ( ¬ ( 𝜑 ∨ 𝜓 ) → ( ( 𝜒 ∨ ( 𝜑 ∨ 𝜓 ) ) → 𝜒 ) ) | |
| 14 | 8 12 13 | e12 | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) , ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) ▶ 𝜒 ) |
| 15 | 14 | in2 | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) ▶ ( ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) → 𝜒 ) ) |
| 16 | 15 | in1 | ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → ( ( 𝜒 ∨ 𝜑 ∨ 𝜓 ) → 𝜒 ) ) |