Theorem e11 45630

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45511

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45512

This theorem is used by:  e11an  45631  e01  45633  e10  45636  elex2VD  45779  elex22VD  45780  eqsbc2VD  45781  tpid3gVD  45783  3ornot23VD  45788  orbi1rVD  45789  3orbi123VD  45791  sbc3orgVD  45792  ordelordALTVD  45808  sbcim2gVD  45816  trsbcVD  45818  undif3VD  45823  sbcssgVD  45824  csbingVD  45825  onfrALTVD  45832  csbeq2gVD  45833  csbsngVD  45834  csbxpgVD  45835  csbresgVD  45836  csbrngVD  45837  csbima12gALTVD  45838  csbunigVD  45839  csbfv12gALTVD  45840  19.41rgVD  45843  2pm13.193VD  45844  hbimpgVD  45845  ax6e2eqVD  45848  2uasbanhVD  45852  notnotrALTVD  45856