Theorem e10 44727

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

Syntax hints:   → wi 4  (   wvd1 44602

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 44603

This theorem is referenced by:  e10an  44728  en3lpVD  44877  3orbi123VD  44882  sbc3orgVD  44883  exbiriVD  44886  3impexpVD  44888  3impexpbicomVD  44889  al2imVD  44894  equncomVD  44900  trsbcVD  44909  sbcssgVD  44915  csbingVD  44916  onfrALTVD  44923  csbsngVD  44925  csbxpgVD  44926  csbresgVD  44927  csbrngVD  44928  csbima12gALTVD  44929  csbunigVD  44930  csbfv12gALTVD  44931  con5VD  44932  hbimpgVD  44936  hbalgVD  44937  hbexgVD  44938  ax6e2eqVD  44939  ax6e2ndeqVD  44941  e2ebindVD  44944  sb5ALTVD  44945