Theorem e10 45386

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

Syntax hints:   → wi 4  (   wvd1 45261

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 45262

This theorem is referenced by:  e10an  45387  en3lpVD  45536  3orbi123VD  45541  sbc3orgVD  45542  exbiriVD  45545  3impexpVD  45547  3impexpbicomVD  45548  al2imVD  45553  equncomVD  45559  trsbcVD  45568  sbcssgVD  45574  csbingVD  45575  onfrALTVD  45582  csbsngVD  45584  csbxpgVD  45585  csbresgVD  45586  csbrngVD  45587  csbima12gALTVD  45588  csbunigVD  45589  csbfv12gALTVD  45590  con5VD  45591  hbimpgVD  45595  hbalgVD  45596  hbexgVD  45597  ax6e2eqVD  45598  ax6e2ndeqVD  45600  e2ebindVD  45603  sb5ALTVD  45604