Theorem e10 44688

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

Syntax hints:   → wi 4  (   wvd1 44563

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 44564

This theorem is referenced by:  e10an  44689  en3lpVD  44838  3orbi123VD  44843  sbc3orgVD  44844  exbiriVD  44847  3impexpVD  44849  3impexpbicomVD  44850  al2imVD  44855  equncomVD  44861  trsbcVD  44870  sbcssgVD  44876  csbingVD  44877  onfrALTVD  44884  csbsngVD  44886  csbxpgVD  44887  csbresgVD  44888  csbrngVD  44889  csbima12gALTVD  44890  csbunigVD  44891  csbfv12gALTVD  44892  con5VD  44893  hbimpgVD  44897  hbalgVD  44898  hbexgVD  44899  ax6e2eqVD  44900  ax6e2ndeqVD  44902  e2ebindVD  44905  sb5ALTVD  44906