Theorem e10 44935

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

Syntax hints:   → wi 4  (   wvd1 44810

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 44811

This theorem is referenced by:  e10an  44936  en3lpVD  45085  3orbi123VD  45090  sbc3orgVD  45091  exbiriVD  45094  3impexpVD  45096  3impexpbicomVD  45097  al2imVD  45102  equncomVD  45108  trsbcVD  45117  sbcssgVD  45123  csbingVD  45124  onfrALTVD  45131  csbsngVD  45133  csbxpgVD  45134  csbresgVD  45135  csbrngVD  45136  csbima12gALTVD  45137  csbunigVD  45138  csbfv12gALTVD  45139  con5VD  45140  hbimpgVD  45144  hbalgVD  45145  hbexgVD  45146  ax6e2eqVD  45147  ax6e2ndeqVD  45149  e2ebindVD  45152  sb5ALTVD  45153