Theorem e11 45139

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

Syntax hints:   → wi 4  (   wvd1 45020

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 208  df-vd1 45021

This theorem is referenced by:  e11an  45140  e01  45142  e10  45145  elex2VD  45288  elex22VD  45289  eqsbc2VD  45290  tpid3gVD  45292  3ornot23VD  45297  orbi1rVD  45298  3orbi123VD  45300  sbc3orgVD  45301  ordelordALTVD  45317  sbcim2gVD  45325  trsbcVD  45327  undif3VD  45332  sbcssgVD  45333  csbingVD  45334  onfrALTVD  45341  csbeq2gVD  45342  csbsngVD  45343  csbxpgVD  45344  csbresgVD  45345  csbrngVD  45346  csbima12gALTVD  45347  csbunigVD  45348  csbfv12gALTVD  45349  19.41rgVD  45352  2pm13.193VD  45353  hbimpgVD  45354  ax6e2eqVD  45357  2uasbanhVD  45361  notnotrALTVD  45365