Theorem e11 44680

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

Syntax hints:   → wi 4  (   wvd1 44561

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 44562

This theorem is referenced by:  e11an  44681  e01  44683  e10  44686  elex2VD  44829  elex22VD  44830  eqsbc2VD  44831  tpid3gVD  44833  3ornot23VD  44838  orbi1rVD  44839  3orbi123VD  44841  sbc3orgVD  44842  ordelordALTVD  44858  sbcim2gVD  44866  trsbcVD  44868  undif3VD  44873  sbcssgVD  44874  csbingVD  44875  onfrALTVD  44882  csbeq2gVD  44883  csbsngVD  44884  csbxpgVD  44885  csbresgVD  44886  csbrngVD  44887  csbima12gALTVD  44888  csbunigVD  44889  csbfv12gALTVD  44890  19.41rgVD  44893  2pm13.193VD  44894  hbimpgVD  44895  ax6e2eqVD  44898  2uasbanhVD  44902  notnotrALTVD  44906