Theorem e10 45937

Description: A virtual deduction elimination rule (see mpisyl 22). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e10.1	⊢ (   𝜑   ▶   𝜓   )
e10.2	⊢ 𝜒
e10.3	⊢ (𝜓 → (𝜒 → 𝜃))

Assertion

Ref	Expression
e10	⊢ (   𝜑   ▶   𝜃   )

Proof of Theorem e10

Step	Hyp	Ref	Expression
1		e10.1	. 2 ⊢ (   𝜑   ▶   𝜓   )
2		e10.2	. . 3 ⊢ 𝜒
3	2	vd01 45840	. 2 ⊢ (   𝜑   ▶   𝜒   )
4		e10.3	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
5	1, 3, 4	e11 45931	1 ⊢ (   𝜑   ▶   𝜃   )

This proof depends on syntax axioms:   → wi 4  (   wvd1 45812

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-vd1 45813

This theorem is used by:  e10an  45938  en3lpVD  46087  3orbi123VD  46092  sbc3orgVD  46093  exbiriVD  46096  3impexpVD  46098  3impexpbicomVD  46099  al2imVD  46104  equncomVD  46110  trsbcVD  46119  sbcssgVD  46125  csbingVD  46126  onfrALTVD  46133  csbsngVD  46135  csbxpgVD  46136  csbresgVD  46137  csbrngVD  46138  csbima12gALTVD  46139  csbunigVD  46140  csbfv12gALTVD  46141  con5VD  46142  hbimpgVD  46146  hbalgVD  46147  hbexgVD  46148  ax6e2eqVD  46149  ax6e2ndeqVD  46151  e2ebindVD  46154  sb5ALTVD  46155