Theorem e11 45519

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

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

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 45401

This theorem is used by:  e11an  45520  e01  45522  e10  45525  elex2VD  45668  elex22VD  45669  eqsbc2VD  45670  tpid3gVD  45672  3ornot23VD  45677  orbi1rVD  45678  3orbi123VD  45680  sbc3orgVD  45681  ordelordALTVD  45697  sbcim2gVD  45705  trsbcVD  45707  undif3VD  45712  sbcssgVD  45713  csbingVD  45714  onfrALTVD  45721  csbeq2gVD  45722  csbsngVD  45723  csbxpgVD  45724  csbresgVD  45725  csbrngVD  45726  csbima12gALTVD  45727  csbunigVD  45728  csbfv12gALTVD  45729  19.41rgVD  45732  2pm13.193VD  45733  hbimpgVD  45734  ax6e2eqVD  45737  2uasbanhVD  45741  notnotrALTVD  45745