Theorem e10 44719

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

Syntax hints:   → wi 4  (   wvd1 44594

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 44595

This theorem is referenced by:  e10an  44720  en3lpVD  44869  3orbi123VD  44874  sbc3orgVD  44875  exbiriVD  44878  3impexpVD  44880  3impexpbicomVD  44881  al2imVD  44886  equncomVD  44892  trsbcVD  44901  sbcssgVD  44907  csbingVD  44908  onfrALTVD  44915  csbsngVD  44917  csbxpgVD  44918  csbresgVD  44919  csbrngVD  44920  csbima12gALTVD  44921  csbunigVD  44922  csbfv12gALTVD  44923  con5VD  44924  hbimpgVD  44928  hbalgVD  44929  hbexgVD  44930  ax6e2eqVD  44931  ax6e2ndeqVD  44933  e2ebindVD  44936  sb5ALTVD  44937