Theorem e11 45133

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

Syntax hints:   → wi 4  (   wvd1 45014

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 45015

This theorem is referenced by:  e11an  45134  e01  45136  e10  45139  elex2VD  45282  elex22VD  45283  eqsbc2VD  45284  tpid3gVD  45286  3ornot23VD  45291  orbi1rVD  45292  3orbi123VD  45294  sbc3orgVD  45295  ordelordALTVD  45311  sbcim2gVD  45319  trsbcVD  45321  undif3VD  45326  sbcssgVD  45327  csbingVD  45328  onfrALTVD  45335  csbeq2gVD  45336  csbsngVD  45337  csbxpgVD  45338  csbresgVD  45339  csbrngVD  45340  csbima12gALTVD  45341  csbunigVD  45342  csbfv12gALTVD  45343  19.41rgVD  45346  2pm13.193VD  45347  hbimpgVD  45348  ax6e2eqVD  45351  2uasbanhVD  45355  notnotrALTVD  45359