Theorem e10 44665

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 44568	. 2 ⊢ (   𝜑   ▶   𝜒   )
4		e10.3	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
5	1, 3, 4	e11 44659	1 ⊢ (   𝜑   ▶   𝜃   )

Syntax hints:   → wi 4  (   wvd1 44540

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 44541

This theorem is referenced by:  e10an  44666  en3lpVD  44816  3orbi123VD  44821  sbc3orgVD  44822  exbiriVD  44825  3impexpVD  44827  3impexpbicomVD  44828  al2imVD  44833  equncomVD  44839  trsbcVD  44848  sbcssgVD  44854  csbingVD  44855  onfrALTVD  44862  csbsngVD  44864  csbxpgVD  44865  csbresgVD  44866  csbrngVD  44867  csbima12gALTVD  44868  csbunigVD  44869  csbfv12gALTVD  44870  con5VD  44871  hbimpgVD  44875  hbalgVD  44876  hbexgVD  44877  ax6e2eqVD  44878  ax6e2ndeqVD  44880  e2ebindVD  44883  sb5ALTVD  44884