Theorem e10 45288

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

Syntax hints:   → wi 4  (   wvd1 45163

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 210  df-vd1 45164

This theorem is referenced by:  e10an  45289  en3lpVD  45438  3orbi123VD  45443  sbc3orgVD  45444  exbiriVD  45447  3impexpVD  45449  3impexpbicomVD  45450  al2imVD  45455  equncomVD  45461  trsbcVD  45470  sbcssgVD  45476  csbingVD  45477  onfrALTVD  45484  csbsngVD  45486  csbxpgVD  45487  csbresgVD  45488  csbrngVD  45489  csbima12gALTVD  45490  csbunigVD  45491  csbfv12gALTVD  45492  con5VD  45493  hbimpgVD  45497  hbalgVD  45498  hbexgVD  45499  ax6e2eqVD  45500  ax6e2ndeqVD  45502  e2ebindVD  45505  sb5ALTVD  45506