Theorem e10 44931

Description: A virtual deduction elimination rule (see mpisyl 21). (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 44834	. 2 ⊢ (   𝜑   ▶   𝜒   )
4		e10.3	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
5	1, 3, 4	e11 44925	1 ⊢ (   𝜑   ▶   𝜃   )

Syntax hints:   → wi 4  (   wvd1 44806

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

This theorem is referenced by:  e10an  44932  en3lpVD  45081  3orbi123VD  45086  sbc3orgVD  45087  exbiriVD  45090  3impexpVD  45092  3impexpbicomVD  45093  al2imVD  45098  equncomVD  45104  trsbcVD  45113  sbcssgVD  45119  csbingVD  45120  onfrALTVD  45127  csbsngVD  45129  csbxpgVD  45130  csbresgVD  45131  csbrngVD  45132  csbima12gALTVD  45133  csbunigVD  45134  csbfv12gALTVD  45135  con5VD  45136  hbimpgVD  45140  hbalgVD  45141  hbexgVD  45142  ax6e2eqVD  45143  ax6e2ndeqVD  45145  e2ebindVD  45148  sb5ALTVD  45149