Theorem e12 45554

Description: A virtual deduction elimination rule (see sylsyld 62). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
e12	⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

Proof of Theorem e12

Step	Hyp	Ref	Expression
1		e12.1	. . 3 ⊢ (   𝜑   ▶   𝜓   )
2	1	vd12 45431	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜓   )
3		e12.2	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )
4		e12.3	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	2, 3, 4	e22 45502	1 ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

This proof depends on syntax axioms:   → wi 4  (   wvd1 45400  (   wvd2 45408

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-vd1 45401  df-vd2 45409

This theorem is used by:  e12an  45555  trsspwALT  45648  sspwtr  45651  pwtrVD  45654  snssiALTVD  45657  elex2VD  45668  elex22VD  45669  eqsbc2VD  45670  en3lplem1VD  45673  3ornot23VD  45677  orbi1rVD  45678  19.21a3con13vVD  45682  exbirVD  45683  tratrbVD  45691  ssralv2VD  45696  sbcim2gVD  45705  sbcbiVD  45706  relopabVD  45731  19.41rgVD  45732  ax6e2eqVD  45737  ax6e2ndeqVD  45739  vk15.4jVD  45744  con3ALTVD  45746