Theorem e11 45256

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

Syntax hints:   → wi 4  (   wvd1 45137

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 210  df-vd1 45138

This theorem is referenced by:  e11an  45257  e01  45259  e10  45262  elex2VD  45405  elex22VD  45406  eqsbc2VD  45407  tpid3gVD  45409  3ornot23VD  45414  orbi1rVD  45415  3orbi123VD  45417  sbc3orgVD  45418  ordelordALTVD  45434  sbcim2gVD  45442  trsbcVD  45444  undif3VD  45449  sbcssgVD  45450  csbingVD  45451  onfrALTVD  45458  csbeq2gVD  45459  csbsngVD  45460  csbxpgVD  45461  csbresgVD  45462  csbrngVD  45463  csbima12gALTVD  45464  csbunigVD  45465  csbfv12gALTVD  45466  19.41rgVD  45469  2pm13.193VD  45470  hbimpgVD  45471  ax6e2eqVD  45474  2uasbanhVD  45478  notnotrALTVD  45482