Theorem 3ornot23VD 44867

Description: Virtual deduction proof of 3ornot23 44529. 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::	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   (¬ 𝜑 ∧ ¬ 𝜓)   )
2::	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ 𝜑 ∨ 𝜓)   )
3:1,?: e1a 44647	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ 𝜑   )
4:1,?: e1a 44647	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ 𝜓   )
5:3,4,?: e11 44708	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ (𝜑 ∨ 𝜓)   )
6:2,?: e2 44651	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ (𝜑 ∨ 𝜓))   )
7:5,6,?: e12 44744	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   𝜒   )
8:7:	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒)   )
qed:8:	⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒))

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
3ornot23VD	⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒))

Proof of Theorem 3ornot23VD

Step	Hyp	Ref	Expression
1		idn1 44594	. . . . . 6 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   (¬ 𝜑 ∧ ¬ 𝜓)   )
2		simpl 482	. . . . . 6 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
3	1, 2	e1a 44647	. . . . 5 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶    ¬ 𝜑   )
4		simpr 484	. . . . . 6 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
5	1, 4	e1a 44647	. . . . 5 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶    ¬ 𝜓   )
6		ioran 986	. . . . . 6 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
7	6	simplbi2 500	. . . . 5 ⊢ (¬ 𝜑 → (¬ 𝜓 → ¬ (𝜑 ∨ 𝜓)))
8	3, 5, 7	e11 44708	. . . 4 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶    ¬ (𝜑 ∨ 𝜓)   )
9		idn2 44633	. . . . 5 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ 𝜑 ∨ 𝜓)   )
10		3orass 1090	. . . . . 6 ⊢ ((𝜒 ∨ 𝜑 ∨ 𝜓) ↔ (𝜒 ∨ (𝜑 ∨ 𝜓)))
11	10	biimpi 216	. . . . 5 ⊢ ((𝜒 ∨ 𝜑 ∨ 𝜓) → (𝜒 ∨ (𝜑 ∨ 𝜓)))
12	9, 11	e2 44651	. . . 4 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ (𝜑 ∨ 𝜓))   )
13		orel2 891	. . . 4 ⊢ (¬ (𝜑 ∨ 𝜓) → ((𝜒 ∨ (𝜑 ∨ 𝜓)) → 𝜒))
14	8, 12, 13	e12 44744	. . 3 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   𝜒   )
15	14	in2 44625	. 2 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒)   )
16	15	in1 44591	1 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848   ∨ w3o 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-vd1 44590  df-vd2 44598

This theorem is referenced by: (None)