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  44815  elex22VD  44816  eqsbc2VD  44817  tpid3gVD  44819  3ornot23VD  44824  orbi1rVD  44825  3orbi123VD  44827  sbc3orgVD  44828  ordelordALTVD  44844  sbcim2gVD  44852  trsbcVD  44854  undif3VD  44859  sbcssgVD  44860  csbingVD  44861  onfrALTVD  44868  csbeq2gVD  44869  csbsngVD  44870  csbxpgVD  44871  csbresgVD  44872  csbrngVD  44873  csbima12gALTVD  44874  csbunigVD  44875  csbfv12gALTVD  44876  19.41rgVD  44879  2pm13.193VD  44880  hbimpgVD  44881  ax6e2eqVD  44884  2uasbanhVD  44888  notnotrALTVD  44892