Theorem e10 44671

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

Syntax hints:   → wi 4  (   wvd1 44546

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 44547

This theorem is referenced by:  e10an  44672  en3lpVD  44822  3orbi123VD  44827  sbc3orgVD  44828  exbiriVD  44831  3impexpVD  44833  3impexpbicomVD  44834  al2imVD  44839  equncomVD  44845  trsbcVD  44854  sbcssgVD  44860  csbingVD  44861  onfrALTVD  44868  csbsngVD  44870  csbxpgVD  44871  csbresgVD  44872  csbrngVD  44873  csbima12gALTVD  44874  csbunigVD  44875  csbfv12gALTVD  44876  con5VD  44877  hbimpgVD  44881  hbalgVD  44882  hbexgVD  44883  ax6e2eqVD  44884  ax6e2ndeqVD  44886  e2ebindVD  44889  sb5ALTVD  44890