Theorem e11 42197

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

Syntax hints:   → wi 4  (   wvd1 42078

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 42079

This theorem is referenced by:  e11an  42198  e01  42200  e10  42203  elex2VD  42347  elex22VD  42348  eqsbc2VD  42349  tpid3gVD  42351  3ornot23VD  42356  orbi1rVD  42357  3orbi123VD  42359  sbc3orgVD  42360  ordelordALTVD  42376  sbcim2gVD  42384  trsbcVD  42386  undif3VD  42391  sbcssgVD  42392  csbingVD  42393  onfrALTVD  42400  csbeq2gVD  42401  csbsngVD  42402  csbxpgVD  42403  csbresgVD  42404  csbrngVD  42405  csbima12gALTVD  42406  csbunigVD  42407  csbfv12gALTVD  42408  19.41rgVD  42411  2pm13.193VD  42412  hbimpgVD  42413  ax6e2eqVD  42416  2uasbanhVD  42420  notnotrALTVD  42424