Theorem e10 44714

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

Syntax hints:   → wi 4  (   wvd1 44589

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 44590

This theorem is referenced by:  e10an  44715  en3lpVD  44865  3orbi123VD  44870  sbc3orgVD  44871  exbiriVD  44874  3impexpVD  44876  3impexpbicomVD  44877  al2imVD  44882  equncomVD  44888  trsbcVD  44897  sbcssgVD  44903  csbingVD  44904  onfrALTVD  44911  csbsngVD  44913  csbxpgVD  44914  csbresgVD  44915  csbrngVD  44916  csbima12gALTVD  44917  csbunigVD  44918  csbfv12gALTVD  44919  con5VD  44920  hbimpgVD  44924  hbalgVD  44925  hbexgVD  44926  ax6e2eqVD  44927  ax6e2ndeqVD  44929  e2ebindVD  44932  sb5ALTVD  44933