Theorem e10 45436

Description: A virtual deduction elimination rule (see mpisyl 22). (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 45339	. 2 ⊢ (   𝜑   ▶   𝜒   )
4		e10.3	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
5	1, 3, 4	e11 45430	1 ⊢ (   𝜑   ▶   𝜃   )

This proof depends on syntax axioms:   → wi 4  (   wvd1 45311

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45312

This theorem is used by:  e10an  45437  en3lpVD  45586  3orbi123VD  45591  sbc3orgVD  45592  exbiriVD  45595  3impexpVD  45597  3impexpbicomVD  45598  al2imVD  45603  equncomVD  45609  trsbcVD  45618  sbcssgVD  45624  csbingVD  45625  onfrALTVD  45632  csbsngVD  45634  csbxpgVD  45635  csbresgVD  45636  csbrngVD  45637  csbima12gALTVD  45638  csbunigVD  45639  csbfv12gALTVD  45640  con5VD  45641  hbimpgVD  45645  hbalgVD  45646  hbexgVD  45647  ax6e2eqVD  45648  ax6e2ndeqVD  45650  e2ebindVD  45653  sb5ALTVD  45654