Theorem e11 45672

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

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

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 45554

This theorem is used by:  e11an  45673  e01  45675  e10  45678  elex2VD  45821  elex22VD  45822  eqsbc2VD  45823  tpid3gVD  45825  3ornot23VD  45830  orbi1rVD  45831  3orbi123VD  45833  sbc3orgVD  45834  ordelordALTVD  45850  sbcim2gVD  45858  trsbcVD  45860  undif3VD  45865  sbcssgVD  45866  csbingVD  45867  onfrALTVD  45874  csbeq2gVD  45875  csbsngVD  45876  csbxpgVD  45877  csbresgVD  45878  csbrngVD  45879  csbima12gALTVD  45880  csbunigVD  45881  csbfv12gALTVD  45882  19.41rgVD  45885  2pm13.193VD  45886  hbimpgVD  45887  ax6e2eqVD  45890  2uasbanhVD  45894  notnotrALTVD  45898