Theorem e10 44691

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

Syntax hints:   → wi 4  (   wvd1 44566

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 44567

This theorem is referenced by:  e10an  44692  en3lpVD  44841  3orbi123VD  44846  sbc3orgVD  44847  exbiriVD  44850  3impexpVD  44852  3impexpbicomVD  44853  al2imVD  44858  equncomVD  44864  trsbcVD  44873  sbcssgVD  44879  csbingVD  44880  onfrALTVD  44887  csbsngVD  44889  csbxpgVD  44890  csbresgVD  44891  csbrngVD  44892  csbima12gALTVD  44893  csbunigVD  44894  csbfv12gALTVD  44895  con5VD  44896  hbimpgVD  44900  hbalgVD  44901  hbexgVD  44902  ax6e2eqVD  44903  ax6e2ndeqVD  44905  e2ebindVD  44908  sb5ALTVD  44909