Theorem e10 45771

Description: A virtual deduction elimination rule (see mpisyl 22). (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 45674	. 2 ⊢ (   𝜑   ▶   𝜒   )
4		e10.3	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
5	1, 3, 4	e11 45765	1 ⊢ (   𝜑   ▶   𝜃   )

This proof depends on syntax axioms:   → wi 4  (   wvd1 45646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45647

This theorem is used by:  e10an  45772  en3lpVD  45921  3orbi123VD  45926  sbc3orgVD  45927  exbiriVD  45930  3impexpVD  45932  3impexpbicomVD  45933  al2imVD  45938  equncomVD  45944  trsbcVD  45953  sbcssgVD  45959  csbingVD  45960  onfrALTVD  45967  csbsngVD  45969  csbxpgVD  45970  csbresgVD  45971  csbrngVD  45972  csbima12gALTVD  45973  csbunigVD  45974  csbfv12gALTVD  45975  con5VD  45976  hbimpgVD  45980  hbalgVD  45981  hbexgVD  45982  ax6e2eqVD  45983  ax6e2ndeqVD  45985  e2ebindVD  45988  sb5ALTVD  45989