Theorem e10 45047

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

Syntax hints:   → wi 4  (   wvd1 44922

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 44923

This theorem is referenced by:  e10an  45048  en3lpVD  45197  3orbi123VD  45202  sbc3orgVD  45203  exbiriVD  45206  3impexpVD  45208  3impexpbicomVD  45209  al2imVD  45214  equncomVD  45220  trsbcVD  45229  sbcssgVD  45235  csbingVD  45236  onfrALTVD  45243  csbsngVD  45245  csbxpgVD  45246  csbresgVD  45247  csbrngVD  45248  csbima12gALTVD  45249  csbunigVD  45250  csbfv12gALTVD  45251  con5VD  45252  hbimpgVD  45256  hbalgVD  45257  hbexgVD  45258  ax6e2eqVD  45259  ax6e2ndeqVD  45261  e2ebindVD  45264  sb5ALTVD  45265