Theorem e10 45662

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

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

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 45538

This theorem is used by:  e10an  45663  en3lpVD  45812  3orbi123VD  45817  sbc3orgVD  45818  exbiriVD  45821  3impexpVD  45823  3impexpbicomVD  45824  al2imVD  45829  equncomVD  45835  trsbcVD  45844  sbcssgVD  45850  csbingVD  45851  onfrALTVD  45858  csbsngVD  45860  csbxpgVD  45861  csbresgVD  45862  csbrngVD  45863  csbima12gALTVD  45864  csbunigVD  45865  csbfv12gALTVD  45866  con5VD  45867  hbimpgVD  45871  hbalgVD  45872  hbexgVD  45873  ax6e2eqVD  45874  ax6e2ndeqVD  45876  e2ebindVD  45879  sb5ALTVD  45880