Theorem e11 44665

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e11.1	⊢ (   𝜑   ▶   𝜓   )
e11.2	⊢ (   𝜑   ▶   𝜒   )
e11.3	⊢ (𝜓 → (𝜒 → 𝜃))

Assertion

Ref	Expression
e11	⊢ (   𝜑   ▶   𝜃   )

Proof of Theorem e11

Step	Hyp	Ref	Expression
1		e11.1	. 2 ⊢ (   𝜑   ▶   𝜓   )
2		e11.2	. 2 ⊢ (   𝜑   ▶   𝜒   )
3		e11.3	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
4	3	a1i 11	. 2 ⊢ (𝜓 → (𝜓 → (𝜒 → 𝜃)))
5	1, 1, 2, 4	e111 44651	1 ⊢ (   𝜑   ▶   𝜃   )

Syntax hints:   → wi 4  (   wvd1 44546

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 44547

This theorem is referenced by:  e11an  44666  e01  44668  e10  44671  elex2VD  44814  elex22VD  44815  eqsbc2VD  44816  tpid3gVD  44818  3ornot23VD  44823  orbi1rVD  44824  3orbi123VD  44826  sbc3orgVD  44827  ordelordALTVD  44843  sbcim2gVD  44851  trsbcVD  44853  undif3VD  44858  sbcssgVD  44859  csbingVD  44860  onfrALTVD  44867  csbeq2gVD  44868  csbsngVD  44869  csbxpgVD  44870  csbresgVD  44871  csbrngVD  44872  csbima12gALTVD  44873  csbunigVD  44874  csbfv12gALTVD  44875  19.41rgVD  44878  2pm13.193VD  44879  hbimpgVD  44880  ax6e2eqVD  44883  2uasbanhVD  44887  notnotrALTVD  44891