Theorem e10 44657

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

Syntax hints:   → wi 4  (   wvd1 44532

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 44533

This theorem is referenced by:  e10an  44658  en3lpVD  44807  3orbi123VD  44812  sbc3orgVD  44813  exbiriVD  44816  3impexpVD  44818  3impexpbicomVD  44819  al2imVD  44824  equncomVD  44830  trsbcVD  44839  sbcssgVD  44845  csbingVD  44846  onfrALTVD  44853  csbsngVD  44855  csbxpgVD  44856  csbresgVD  44857  csbrngVD  44858  csbima12gALTVD  44859  csbunigVD  44860  csbfv12gALTVD  44861  con5VD  44862  hbimpgVD  44866  hbalgVD  44867  hbexgVD  44868  ax6e2eqVD  44869  ax6e2ndeqVD  44871  e2ebindVD  44874  sb5ALTVD  44875