Theorem e11 39230

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

Syntax hints:   → wi 4  (   wvd1 39102

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 197  df-vd1 39103

This theorem is referenced by:  e11an  39231  e01  39233  e10  39236  elex2VD  39387  elex22VD  39388  eqsbc3rVD  39389  tpid3gVD  39391  3ornot23VD  39396  orbi1rVD  39397  3orbi123VD  39399  sbc3orgVD  39400  sbcoreleleqVD  39409  ordelordALTVD  39417  sbcim2gVD  39425  trsbcVD  39427  undif3VD  39432  sbcssgVD  39433  csbingVD  39434  onfrALTVD  39441  csbeq2gVD  39442  csbsngVD  39443  csbxpgVD  39444  csbresgVD  39445  csbrngVD  39446  csbima12gALTVD  39447  csbunigVD  39448  csbfv12gALTVD  39449  19.41rgVD  39452  2pm13.193VD  39453  hbimpgVD  39454  ax6e2eqVD  39457  2uasbanhVD  39461  notnotrALTVD  39465