Theorem e11 45873

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

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

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 45755

This theorem is used by:  e11an  45874  e01  45876  e10  45879  elex2VD  46022  elex22VD  46023  eqsbc2VD  46024  tpid3gVD  46026  3ornot23VD  46031  orbi1rVD  46032  3orbi123VD  46034  sbc3orgVD  46035  ordelordALTVD  46051  sbcim2gVD  46059  trsbcVD  46061  undif3VD  46066  sbcssgVD  46067  csbingVD  46068  onfrALTVD  46075  csbeq2gVD  46076  csbsngVD  46077  csbxpgVD  46078  csbresgVD  46079  csbrngVD  46080  csbima12gALTVD  46081  csbunigVD  46082  csbfv12gALTVD  46083  19.41rgVD  46086  2pm13.193VD  46087  hbimpgVD  46088  ax6e2eqVD  46091  2uasbanhVD  46095  notnotrALTVD  46099