Theorem e10 42203

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

Syntax hints:   → wi 4  (   wvd1 42078

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 42079

This theorem is referenced by:  e10an  42204  en3lpVD  42354  3orbi123VD  42359  sbc3orgVD  42360  exbiriVD  42363  3impexpVD  42365  3impexpbicomVD  42366  al2imVD  42371  equncomVD  42377  trsbcVD  42386  sbcssgVD  42392  csbingVD  42393  onfrALTVD  42400  csbsngVD  42402  csbxpgVD  42403  csbresgVD  42404  csbrngVD  42405  csbima12gALTVD  42406  csbunigVD  42407  csbfv12gALTVD  42408  con5VD  42409  hbimpgVD  42413  hbalgVD  42414  hbexgVD  42415  ax6e2eqVD  42416  ax6e2ndeqVD  42418  e2ebindVD  42421  sb5ALTVD  42422