Theorem e22 41012

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

Syntax hints:   → wi 4  (   wvd2 40918

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 209  df-an 399  df-vd2 40919

This theorem is referenced by:  e22an  41013  e02  41038  e12  41065  e20  41068  e21  41071  sspwtr  41162  pwtrVD  41165  pwtrrVD  41166  elex22VD  41180  tpid3gVD  41183  en3lplem2VD  41185  imbi12VD  41214  truniALTVD  41219  trintALTVD  41221  onfrALTlem3VD  41228  onfrALTlem2VD  41230  ax6e2eqVD  41248  ax6e2ndeqVD  41250  sb5ALTVD  41254