Theorem e10 45231

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

Syntax hints:   → wi 4  (   wvd1 45106

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 45107

This theorem is referenced by:  e10an  45232  en3lpVD  45381  3orbi123VD  45386  sbc3orgVD  45387  exbiriVD  45390  3impexpVD  45392  3impexpbicomVD  45393  al2imVD  45398  equncomVD  45404  trsbcVD  45413  sbcssgVD  45419  csbingVD  45420  onfrALTVD  45427  csbsngVD  45429  csbxpgVD  45430  csbresgVD  45431  csbrngVD  45432  csbima12gALTVD  45433  csbunigVD  45434  csbfv12gALTVD  45435  con5VD  45436  hbimpgVD  45440  hbalgVD  45441  hbexgVD  45442  ax6e2eqVD  45443  ax6e2ndeqVD  45445  e2ebindVD  45448  sb5ALTVD  45449