Theorem e10 45517

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

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

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 45393

This theorem is used by:  e10an  45518  en3lpVD  45667  3orbi123VD  45672  sbc3orgVD  45673  exbiriVD  45676  3impexpVD  45678  3impexpbicomVD  45679  al2imVD  45684  equncomVD  45690  trsbcVD  45699  sbcssgVD  45705  csbingVD  45706  onfrALTVD  45713  csbsngVD  45715  csbxpgVD  45716  csbresgVD  45717  csbrngVD  45718  csbima12gALTVD  45719  csbunigVD  45720  csbfv12gALTVD  45721  con5VD  45722  hbimpgVD  45726  hbalgVD  45727  hbexgVD  45728  ax6e2eqVD  45729  ax6e2ndeqVD  45731  e2ebindVD  45734  sb5ALTVD  45735