Theorem e10 44684

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

Syntax hints:   → wi 4  (   wvd1 44559

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 44560

This theorem is referenced by:  e10an  44685  en3lpVD  44834  3orbi123VD  44839  sbc3orgVD  44840  exbiriVD  44843  3impexpVD  44845  3impexpbicomVD  44846  al2imVD  44851  equncomVD  44857  trsbcVD  44866  sbcssgVD  44872  csbingVD  44873  onfrALTVD  44880  csbsngVD  44882  csbxpgVD  44883  csbresgVD  44884  csbrngVD  44885  csbima12gALTVD  44886  csbunigVD  44887  csbfv12gALTVD  44888  con5VD  44889  hbimpgVD  44893  hbalgVD  44894  hbexgVD  44895  ax6e2eqVD  44896  ax6e2ndeqVD  44898  e2ebindVD  44901  sb5ALTVD  44902