Theorem e11 44727

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

Syntax hints:   → wi 4  (   wvd1 44608

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 44609

This theorem is referenced by:  e11an  44728  e01  44730  e10  44733  elex2VD  44876  elex22VD  44877  eqsbc2VD  44878  tpid3gVD  44880  3ornot23VD  44885  orbi1rVD  44886  3orbi123VD  44888  sbc3orgVD  44889  ordelordALTVD  44905  sbcim2gVD  44913  trsbcVD  44915  undif3VD  44920  sbcssgVD  44921  csbingVD  44922  onfrALTVD  44929  csbeq2gVD  44930  csbsngVD  44931  csbxpgVD  44932  csbresgVD  44933  csbrngVD  44934  csbima12gALTVD  44935  csbunigVD  44936  csbfv12gALTVD  44937  19.41rgVD  44940  2pm13.193VD  44941  hbimpgVD  44942  ax6e2eqVD  44945  2uasbanhVD  44949  notnotrALTVD  44953