Theorem e10 39236

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

Syntax hints:   → wi 4  (   wvd1 39102

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 197  df-vd1 39103

This theorem is referenced by:  e10an  39237  en3lpVD  39394  3orbi123VD  39399  sbc3orgVD  39400  exbiriVD  39403  3impexpVD  39405  3impexpbicomVD  39406  al2imVD  39412  equncomVD  39418  trsbcVD  39427  sbcssgVD  39433  csbingVD  39434  onfrALTVD  39441  csbsngVD  39443  csbxpgVD  39444  csbresgVD  39445  csbrngVD  39446  csbima12gALTVD  39447  csbunigVD  39448  csbfv12gALTVD  39449  con5VD  39450  hbimpgVD  39454  hbalgVD  39455  hbexgVD  39456  ax6e2eqVD  39457  ax6e2ndeqVD  39459  e2ebindVD  39462  sb5ALTVD  39463