Theorem e10 45121

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

Syntax hints:   → wi 4  (   wvd1 44996

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 44997

This theorem is referenced by:  e10an  45122  en3lpVD  45271  3orbi123VD  45276  sbc3orgVD  45277  exbiriVD  45280  3impexpVD  45282  3impexpbicomVD  45283  al2imVD  45288  equncomVD  45294  trsbcVD  45303  sbcssgVD  45309  csbingVD  45310  onfrALTVD  45317  csbsngVD  45319  csbxpgVD  45320  csbresgVD  45321  csbrngVD  45322  csbima12gALTVD  45323  csbunigVD  45324  csbfv12gALTVD  45325  con5VD  45326  hbimpgVD  45330  hbalgVD  45331  hbexgVD  45332  ax6e2eqVD  45333  ax6e2ndeqVD  45335  e2ebindVD  45338  sb5ALTVD  45339