Theorem e11 44808

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

Syntax hints:   → wi 4  (   wvd1 44689

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 207  df-vd1 44690

This theorem is referenced by:  e11an  44809  e01  44811  e10  44814  elex2VD  44957  elex22VD  44958  eqsbc2VD  44959  tpid3gVD  44961  3ornot23VD  44966  orbi1rVD  44967  3orbi123VD  44969  sbc3orgVD  44970  ordelordALTVD  44986  sbcim2gVD  44994  trsbcVD  44996  undif3VD  45001  sbcssgVD  45002  csbingVD  45003  onfrALTVD  45010  csbeq2gVD  45011  csbsngVD  45012  csbxpgVD  45013  csbresgVD  45014  csbrngVD  45015  csbima12gALTVD  45016  csbunigVD  45017  csbfv12gALTVD  45018  19.41rgVD  45021  2pm13.193VD  45022  hbimpgVD  45023  ax6e2eqVD  45026  2uasbanhVD  45030  notnotrALTVD  45034