Theorem e11 42308

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

Syntax hints:   → wi 4  (   wvd1 42189

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 42190

This theorem is referenced by:  e11an  42309  e01  42311  e10  42314  elex2VD  42458  elex22VD  42459  eqsbc2VD  42460  tpid3gVD  42462  3ornot23VD  42467  orbi1rVD  42468  3orbi123VD  42470  sbc3orgVD  42471  ordelordALTVD  42487  sbcim2gVD  42495  trsbcVD  42497  undif3VD  42502  sbcssgVD  42503  csbingVD  42504  onfrALTVD  42511  csbeq2gVD  42512  csbsngVD  42513  csbxpgVD  42514  csbresgVD  42515  csbrngVD  42516  csbima12gALTVD  42517  csbunigVD  42518  csbfv12gALTVD  42519  19.41rgVD  42522  2pm13.193VD  42523  hbimpgVD  42524  ax6e2eqVD  42527  2uasbanhVD  42531  notnotrALTVD  42535