Theorem in2 45790

Description: The virtual deduction introduction rule of converting the end virtual hypothesis of 2 virtual hypotheses into an antecedent. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
in2.1	⊢ (   𝜑   ,   𝜓   ▶   𝜒   )

Assertion

Ref	Expression
in2	⊢ (   𝜑   ▶   (𝜓 → 𝜒)   )

Proof of Theorem in2

Step	Hyp	Ref	Expression
1		in2.1	. . 3 ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
2	1	dfvd2i 45770	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	dfvd1ir 45758	1 ⊢ (   𝜑   ▶   (𝜓 → 𝜒)   )

This proof depends on syntax axioms:   → wi 4  (   wvd1 45754  (   wvd2 45762

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 45755  df-vd2 45763

This theorem is used by:  e223  45820  trsspwALT  46002  sspwtr  46005  pwtrVD  46008  pwtrrVD  46009  snssiALTVD  46011  sstrALT2VD  46018  suctrALT2VD  46020  elex2VD  46022  elex22VD  46023  eqsbc2VD  46024  tpid3gVD  46026  en3lplem1VD  46027  en3lplem2VD  46028  3ornot23VD  46031  orbi1rVD  46032  19.21a3con13vVD  46036  exbirVD  46037  exbiriVD  46038  rspsbc2VD  46039  tratrbVD  46045  syl5impVD  46047  ssralv2VD  46050  imbi12VD  46057  imbi13VD  46058  sbcim2gVD  46059  sbcbiVD  46060  truniALTVD  46062  trintALTVD  46064  onfrALTVD  46075  relopabVD  46085  19.41rgVD  46086  hbimpgVD  46088  ax6e2eqVD  46091  ax6e2ndeqVD  46093  con3ALTVD  46100