Theorem 3ornot23VD 42356

Description: Virtual deduction proof of 3ornot23 42018. 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 42136	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ 𝜑   )
4:1,?: e1a 42136	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ 𝜓   )
5:3,4,?: e11 42197	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ (𝜑 ∨ 𝜓)   )
6:2,?: e2 42140	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ (𝜑 ∨ 𝜓))   )
7:5,6,?: e12 42233	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   𝜒   )
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 42083	. . . . . 6 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   (¬ 𝜑 ∧ ¬ 𝜓)   )
2		simpl 482	. . . . . 6 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
3	1, 2	e1a 42136	. . . . 5 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶    ¬ 𝜑   )
4		simpr 484	. . . . . 6 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
5	1, 4	e1a 42136	. . . . 5 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶    ¬ 𝜓   )
6		ioran 980	. . . . . 6 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
7	6	simplbi2 500	. . . . 5 ⊢ (¬ 𝜑 → (¬ 𝜓 → ¬ (𝜑 ∨ 𝜓)))
8	3, 5, 7	e11 42197	. . . 4 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶    ¬ (𝜑 ∨ 𝜓)   )
9		idn2 42122	. . . . 5 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ 𝜑 ∨ 𝜓)   )
10		3orass 1088	. . . . . 6 ⊢ ((𝜒 ∨ 𝜑 ∨ 𝜓) ↔ (𝜒 ∨ (𝜑 ∨ 𝜓)))
11	10	biimpi 215	. . . . 5 ⊢ ((𝜒 ∨ 𝜑 ∨ 𝜓) → (𝜒 ∨ (𝜑 ∨ 𝜓)))
12	9, 11	e2 42140	. . . 4 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ (𝜑 ∨ 𝜓))   )
13		orel2 887	. . . 4 ⊢ (¬ (𝜑 ∨ 𝜓) → ((𝜒 ∨ (𝜑 ∨ 𝜓)) → 𝜒))
14	8, 12, 13	e12 42233	. . 3 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   𝜒   )
15	14	in2 42114	. 2 ⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒)   )
16	15	in1 42080	1 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 843   ∨ w3o 1084

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 396  df-or 844  df-3or 1086  df-vd1 42079  df-vd2 42087

This theorem is referenced by: (None)