Theorem e11 44099

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

Syntax hints:   → wi 4  (   wvd1 43980

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 206  df-vd1 43981

This theorem is referenced by:  e11an  44100  e01  44102  e10  44105  elex2VD  44249  elex22VD  44250  eqsbc2VD  44251  tpid3gVD  44253  3ornot23VD  44258  orbi1rVD  44259  3orbi123VD  44261  sbc3orgVD  44262  ordelordALTVD  44278  sbcim2gVD  44286  trsbcVD  44288  undif3VD  44293  sbcssgVD  44294  csbingVD  44295  onfrALTVD  44302  csbeq2gVD  44303  csbsngVD  44304  csbxpgVD  44305  csbresgVD  44306  csbrngVD  44307  csbima12gALTVD  44308  csbunigVD  44309  csbfv12gALTVD  44310  19.41rgVD  44313  2pm13.193VD  44314  hbimpgVD  44315  ax6e2eqVD  44318  2uasbanhVD  44322  notnotrALTVD  44326