Theorem 3ornot23VD 42467

Description: Virtual deduction proof of 3ornot23 42129. 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 42247	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ 𝜑   )
4:1,?: e1a 42247	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ 𝜓   )
5:3,4,?: e11 42308	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ (𝜑 ∨ 𝜓)   )
6:2,?: e2 42251	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ (𝜑 ∨ 𝜓))   )
7:5,6,?: e12 42344	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   𝜒   )
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 42194	. . . . . 6 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   (¬ 𝜑 ∧ ¬ 𝜓)   )
2		simpl 483	. . . . . 6 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
3	1, 2	e1a 42247	. . . . 5 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶    ¬ 𝜑   )
4		simpr 485	. . . . . 6 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
5	1, 4	e1a 42247	. . . . 5 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶    ¬ 𝜓   )
6		ioran 981	. . . . . 6 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
7	6	simplbi2 501	. . . . 5 ⊢ (¬ 𝜑 → (¬ 𝜓 → ¬ (𝜑 ∨ 𝜓)))
8	3, 5, 7	e11 42308	. . . 4 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶    ¬ (𝜑 ∨ 𝜓)   )
9		idn2 42233	. . . . 5 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ 𝜑 ∨ 𝜓)   )
10		3orass 1089	. . . . . 6 ⊢ ((𝜒 ∨ 𝜑 ∨ 𝜓) ↔ (𝜒 ∨ (𝜑 ∨ 𝜓)))
11	10	biimpi 215	. . . . 5 ⊢ ((𝜒 ∨ 𝜑 ∨ 𝜓) → (𝜒 ∨ (𝜑 ∨ 𝜓)))
12	9, 11	e2 42251	. . . 4 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ (𝜑 ∨ 𝜓))   )
13		orel2 888	. . . 4 ⊢ (¬ (𝜑 ∨ 𝜓) → ((𝜒 ∨ (𝜑 ∨ 𝜓)) → 𝜒))
14	8, 12, 13	e12 42344	. . 3 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   𝜒   )
15	14	in2 42225	. 2 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒)   )
16	15	in1 42191	1 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 844   ∨ w3o 1085

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 206  df-an 397  df-or 845  df-3or 1087  df-vd1 42190  df-vd2 42198

This theorem is referenced by: (None)