Theorem e22 44912

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e22.1	⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
e22.2	⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
e22.3	⊢ (𝜒 → (𝜃 → 𝜏))

Assertion

Ref	Expression
e22	⊢ (   𝜑   ,   𝜓   ▶   𝜏   )

Proof of Theorem e22

Step	Hyp	Ref	Expression
1		e22.1	. 2 ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
2		e22.2	. 2 ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
3		e22.3	. . 3 ⊢ (𝜒 → (𝜃 → 𝜏))
4	3	a1i 11	. 2 ⊢ (𝜒 → (𝜒 → (𝜃 → 𝜏)))
5	1, 1, 2, 4	e222 44877	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )

Syntax hints:   → wi 4  (   wvd2 44818

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-an 396  df-vd2 44819

This theorem is referenced by:  e22an  44913  e02  44938  e12  44964  e20  44967  e21  44970  sspwtr  45061  pwtrVD  45064  pwtrrVD  45065  elex22VD  45079  tpid3gVD  45082  en3lplem2VD  45084  imbi12VD  45113  truniALTVD  45118  trintALTVD  45120  onfrALTlem3VD  45127  onfrALTlem2VD  45129  ax6e2eqVD  45147  ax6e2ndeqVD  45149  sb5ALTVD  45153