Theorem e10 41048

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

Syntax hints:   → wi 4  (   wvd1 40923

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 209  df-vd1 40924

This theorem is referenced by:  e10an  41049  en3lpVD  41199  3orbi123VD  41204  sbc3orgVD  41205  exbiriVD  41208  3impexpVD  41210  3impexpbicomVD  41211  al2imVD  41216  equncomVD  41222  trsbcVD  41231  sbcssgVD  41237  csbingVD  41238  onfrALTVD  41245  csbsngVD  41247  csbxpgVD  41248  csbresgVD  41249  csbrngVD  41250  csbima12gALTVD  41251  csbunigVD  41252  csbfv12gALTVD  41253  con5VD  41254  hbimpgVD  41258  hbalgVD  41259  hbexgVD  41260  ax6e2eqVD  41261  ax6e2ndeqVD  41263  e2ebindVD  41266  sb5ALTVD  41267