Theorem e10 41400

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

Syntax hints:   → wi 4  (   wvd1 41275

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 210  df-vd1 41276

This theorem is referenced by:  e10an  41401  en3lpVD  41551  3orbi123VD  41556  sbc3orgVD  41557  exbiriVD  41560  3impexpVD  41562  3impexpbicomVD  41563  al2imVD  41568  equncomVD  41574  trsbcVD  41583  sbcssgVD  41589  csbingVD  41590  onfrALTVD  41597  csbsngVD  41599  csbxpgVD  41600  csbresgVD  41601  csbrngVD  41602  csbima12gALTVD  41603  csbunigVD  41604  csbfv12gALTVD  41605  con5VD  41606  hbimpgVD  41610  hbalgVD  41611  hbexgVD  41612  ax6e2eqVD  41613  ax6e2ndeqVD  41615  e2ebindVD  41618  sb5ALTVD  41619