Theorem e11 44929

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

Syntax hints:   → wi 4  (   wvd1 44810

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 44811

This theorem is referenced by:  e11an  44930  e01  44932  e10  44935  elex2VD  45078  elex22VD  45079  eqsbc2VD  45080  tpid3gVD  45082  3ornot23VD  45087  orbi1rVD  45088  3orbi123VD  45090  sbc3orgVD  45091  ordelordALTVD  45107  sbcim2gVD  45115  trsbcVD  45117  undif3VD  45122  sbcssgVD  45123  csbingVD  45124  onfrALTVD  45131  csbeq2gVD  45132  csbsngVD  45133  csbxpgVD  45134  csbresgVD  45135  csbrngVD  45136  csbima12gALTVD  45137  csbunigVD  45138  csbfv12gALTVD  45139  19.41rgVD  45142  2pm13.193VD  45143  hbimpgVD  45144  ax6e2eqVD  45147  2uasbanhVD  45151  notnotrALTVD  45155