Theorem e10 43445

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

Syntax hints:   → wi 4  (   wvd1 43320

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 206  df-vd1 43321

This theorem is referenced by:  e10an  43446  en3lpVD  43596  3orbi123VD  43601  sbc3orgVD  43602  exbiriVD  43605  3impexpVD  43607  3impexpbicomVD  43608  al2imVD  43613  equncomVD  43619  trsbcVD  43628  sbcssgVD  43634  csbingVD  43635  onfrALTVD  43642  csbsngVD  43644  csbxpgVD  43645  csbresgVD  43646  csbrngVD  43647  csbima12gALTVD  43648  csbunigVD  43649  csbfv12gALTVD  43650  con5VD  43651  hbimpgVD  43655  hbalgVD  43656  hbexgVD  43657  ax6e2eqVD  43658  ax6e2ndeqVD  43660  e2ebindVD  43663  sb5ALTVD  43664