Theorem e10 44851

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

Syntax hints:   → wi 4  (   wvd1 44726

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 44727

This theorem is referenced by:  e10an  44852  en3lpVD  45001  3orbi123VD  45006  sbc3orgVD  45007  exbiriVD  45010  3impexpVD  45012  3impexpbicomVD  45013  al2imVD  45018  equncomVD  45024  trsbcVD  45033  sbcssgVD  45039  csbingVD  45040  onfrALTVD  45047  csbsngVD  45049  csbxpgVD  45050  csbresgVD  45051  csbrngVD  45052  csbima12gALTVD  45053  csbunigVD  45054  csbfv12gALTVD  45055  con5VD  45056  hbimpgVD  45060  hbalgVD  45061  hbexgVD  45062  ax6e2eqVD  45063  ax6e2ndeqVD  45065  e2ebindVD  45068  sb5ALTVD  45069