Theorem e11 44678

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 44664	1 ⊢ (   𝜑   ▶   𝜃   )

Syntax hints:   → wi 4  (   wvd1 44559

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 44560

This theorem is referenced by:  e11an  44679  e01  44681  e10  44684  elex2VD  44827  elex22VD  44828  eqsbc2VD  44829  tpid3gVD  44831  3ornot23VD  44836  orbi1rVD  44837  3orbi123VD  44839  sbc3orgVD  44840  ordelordALTVD  44856  sbcim2gVD  44864  trsbcVD  44866  undif3VD  44871  sbcssgVD  44872  csbingVD  44873  onfrALTVD  44880  csbeq2gVD  44881  csbsngVD  44882  csbxpgVD  44883  csbresgVD  44884  csbrngVD  44885  csbima12gALTVD  44886  csbunigVD  44887  csbfv12gALTVD  44888  19.41rgVD  44891  2pm13.193VD  44892  hbimpgVD  44893  ax6e2eqVD  44896  2uasbanhVD  44900  notnotrALTVD  44904