Theorem e11 44713

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

Syntax hints:   → wi 4  (   wvd1 44594

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 44595

This theorem is referenced by:  e11an  44714  e01  44716  e10  44719  elex2VD  44863  elex22VD  44864  eqsbc2VD  44865  tpid3gVD  44867  3ornot23VD  44872  orbi1rVD  44873  3orbi123VD  44875  sbc3orgVD  44876  ordelordALTVD  44892  sbcim2gVD  44900  trsbcVD  44902  undif3VD  44907  sbcssgVD  44908  csbingVD  44909  onfrALTVD  44916  csbeq2gVD  44917  csbsngVD  44918  csbxpgVD  44919  csbresgVD  44920  csbrngVD  44921  csbima12gALTVD  44922  csbunigVD  44923  csbfv12gALTVD  44924  19.41rgVD  44927  2pm13.193VD  44928  hbimpgVD  44929  ax6e2eqVD  44932  2uasbanhVD  44936  notnotrALTVD  44940