Theorem e10 45138

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

Syntax hints:   → wi 4  (   wvd1 45013

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 208  df-vd1 45014

This theorem is referenced by:  e10an  45139  en3lpVD  45288  3orbi123VD  45293  sbc3orgVD  45294  exbiriVD  45297  3impexpVD  45299  3impexpbicomVD  45300  al2imVD  45305  equncomVD  45311  trsbcVD  45320  sbcssgVD  45326  csbingVD  45327  onfrALTVD  45334  csbsngVD  45336  csbxpgVD  45337  csbresgVD  45338  csbrngVD  45339  csbima12gALTVD  45340  csbunigVD  45341  csbfv12gALTVD  45342  con5VD  45343  hbimpgVD  45347  hbalgVD  45348  hbexgVD  45349  ax6e2eqVD  45350  ax6e2ndeqVD  45352  e2ebindVD  45355  sb5ALTVD  45356