Theorem e11 44659

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

Syntax hints:   → wi 4  (   wvd1 44540

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 44541

This theorem is referenced by:  e11an  44660  e01  44662  e10  44665  elex2VD  44809  elex22VD  44810  eqsbc2VD  44811  tpid3gVD  44813  3ornot23VD  44818  orbi1rVD  44819  3orbi123VD  44821  sbc3orgVD  44822  ordelordALTVD  44838  sbcim2gVD  44846  trsbcVD  44848  undif3VD  44853  sbcssgVD  44854  csbingVD  44855  onfrALTVD  44862  csbeq2gVD  44863  csbsngVD  44864  csbxpgVD  44865  csbresgVD  44866  csbrngVD  44867  csbima12gALTVD  44868  csbunigVD  44869  csbfv12gALTVD  44870  19.41rgVD  44873  2pm13.193VD  44874  hbimpgVD  44875  ax6e2eqVD  44878  2uasbanhVD  44882  notnotrALTVD  44886