Theorem e11 44686

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

Syntax hints:   → wi 4  (   wvd1 44567

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 44568

This theorem is referenced by:  e11an  44687  e01  44689  e10  44692  elex2VD  44836  elex22VD  44837  eqsbc2VD  44838  tpid3gVD  44840  3ornot23VD  44845  orbi1rVD  44846  3orbi123VD  44848  sbc3orgVD  44849  ordelordALTVD  44865  sbcim2gVD  44873  trsbcVD  44875  undif3VD  44880  sbcssgVD  44881  csbingVD  44882  onfrALTVD  44889  csbeq2gVD  44890  csbsngVD  44891  csbxpgVD  44892  csbresgVD  44893  csbrngVD  44894  csbima12gALTVD  44895  csbunigVD  44896  csbfv12gALTVD  44897  19.41rgVD  44900  2pm13.193VD  44901  hbimpgVD  44902  ax6e2eqVD  44905  2uasbanhVD  44909  notnotrALTVD  44913