Theorem simplbi2VD 45612

Description: Virtual deduction proof of simplbi2 506. 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.

h1::	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3:1,?: e0a 45538	⊢ ((𝜓 ∧ 𝜒) → 𝜑)
qed:3,?: e0a 45538	⊢ (𝜓 → (𝜒 → 𝜑))

The proof of simplbi2 506 was automatically derived from it. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
pm3.26bi2VD.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simplbi2VD	⊢ (𝜓 → (𝜒 → 𝜑))

Proof of Theorem simplbi2VD

Step	Hyp	Ref	Expression
1		pm3.26bi2VD.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		biimpr 223	. . 3 ⊢ ((𝜑 ↔ (𝜓 ∧ 𝜒)) → ((𝜓 ∧ 𝜒) → 𝜑))
3	1, 2	e0a 45538	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜑)
4		pm3.3 454	. 2 ⊢ (((𝜓 ∧ 𝜒) → 𝜑) → (𝜓 → (𝜒 → 𝜑)))
5	3, 4	e0a 45538	1 ⊢ (𝜓 → (𝜒 → 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by: (None)