Theorem e10 42314

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

Syntax hints:   → wi 4  (   wvd1 42189

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 42190

This theorem is referenced by:  e10an  42315  en3lpVD  42465  3orbi123VD  42470  sbc3orgVD  42471  exbiriVD  42474  3impexpVD  42476  3impexpbicomVD  42477  al2imVD  42482  equncomVD  42488  trsbcVD  42497  sbcssgVD  42503  csbingVD  42504  onfrALTVD  42511  csbsngVD  42513  csbxpgVD  42514  csbresgVD  42515  csbrngVD  42516  csbima12gALTVD  42517  csbunigVD  42518  csbfv12gALTVD  42519  con5VD  42520  hbimpgVD  42524  hbalgVD  42525  hbexgVD  42526  ax6e2eqVD  42527  ax6e2ndeqVD  42529  e2ebindVD  42532  sb5ALTVD  42533