Theorem e10 43455

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

Syntax hints:   → wi 4  (   wvd1 43330

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 206  df-vd1 43331

This theorem is referenced by:  e10an  43456  en3lpVD  43606  3orbi123VD  43611  sbc3orgVD  43612  exbiriVD  43615  3impexpVD  43617  3impexpbicomVD  43618  al2imVD  43623  equncomVD  43629  trsbcVD  43638  sbcssgVD  43644  csbingVD  43645  onfrALTVD  43652  csbsngVD  43654  csbxpgVD  43655  csbresgVD  43656  csbrngVD  43657  csbima12gALTVD  43658  csbunigVD  43659  csbfv12gALTVD  43660  con5VD  43661  hbimpgVD  43665  hbalgVD  43666  hbexgVD  43667  ax6e2eqVD  43668  ax6e2ndeqVD  43670  e2ebindVD  43673  sb5ALTVD  43674