Theorem e11 42289

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

Syntax hints:   → wi 4  (   wvd1 42170

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 206  df-vd1 42171

This theorem is referenced by:  e11an  42290  e01  42292  e10  42295  elex2VD  42439  elex22VD  42440  eqsbc2VD  42441  tpid3gVD  42443  3ornot23VD  42448  orbi1rVD  42449  3orbi123VD  42451  sbc3orgVD  42452  ordelordALTVD  42468  sbcim2gVD  42476  trsbcVD  42478  undif3VD  42483  sbcssgVD  42484  csbingVD  42485  onfrALTVD  42492  csbeq2gVD  42493  csbsngVD  42494  csbxpgVD  42495  csbresgVD  42496  csbrngVD  42497  csbima12gALTVD  42498  csbunigVD  42499  csbfv12gALTVD  42500  19.41rgVD  42503  2pm13.193VD  42504  hbimpgVD  42505  ax6e2eqVD  42508  2uasbanhVD  42512  notnotrALTVD  42516