Theorem e22 44788

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 44753	1 ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )

Syntax hints:   → wi 4  (   wvd2 44694

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 44695

This theorem is referenced by:  e22an  44789  e02  44814  e12  44840  e20  44843  e21  44846  sspwtr  44937  pwtrVD  44940  pwtrrVD  44941  elex22VD  44955  tpid3gVD  44958  en3lplem2VD  44960  imbi12VD  44989  truniALTVD  44994  trintALTVD  44996  onfrALTlem3VD  45003  onfrALTlem2VD  45005  ax6e2eqVD  45023  ax6e2ndeqVD  45025  sb5ALTVD  45029