Theorem e11 45380

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

Syntax hints:   → wi 4  (   wvd1 45261

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 210  df-vd1 45262

This theorem is referenced by:  e11an  45381  e01  45383  e10  45386  elex2VD  45529  elex22VD  45530  eqsbc2VD  45531  tpid3gVD  45533  3ornot23VD  45538  orbi1rVD  45539  3orbi123VD  45541  sbc3orgVD  45542  ordelordALTVD  45558  sbcim2gVD  45566  trsbcVD  45568  undif3VD  45573  sbcssgVD  45574  csbingVD  45575  onfrALTVD  45582  csbeq2gVD  45583  csbsngVD  45584  csbxpgVD  45585  csbresgVD  45586  csbrngVD  45587  csbima12gALTVD  45588  csbunigVD  45589  csbfv12gALTVD  45590  19.41rgVD  45593  2pm13.193VD  45594  hbimpgVD  45595  ax6e2eqVD  45598  2uasbanhVD  45602  notnotrALTVD  45606