Theorem e10 45139

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

Syntax hints:   → wi 4  (   wvd1 45014

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 45015

This theorem is referenced by:  e10an  45140  en3lpVD  45289  3orbi123VD  45294  sbc3orgVD  45295  exbiriVD  45298  3impexpVD  45300  3impexpbicomVD  45301  al2imVD  45306  equncomVD  45312  trsbcVD  45321  sbcssgVD  45327  csbingVD  45328  onfrALTVD  45335  csbsngVD  45337  csbxpgVD  45338  csbresgVD  45339  csbrngVD  45340  csbima12gALTVD  45341  csbunigVD  45342  csbfv12gALTVD  45343  con5VD  45344  hbimpgVD  45348  hbalgVD  45349  hbexgVD  45350  ax6e2eqVD  45351  ax6e2ndeqVD  45353  e2ebindVD  45356  sb5ALTVD  45357