Theorem in2 44602

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 44582	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	dfvd1ir 44570	1 ⊢ (   𝜑   ▶   (𝜓 → 𝜒)   )

Syntax hints:   → wi 4  (   wvd1 44566  (   wvd2 44574

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-vd1 44567  df-vd2 44575

This theorem is referenced by:  e223  44632  trsspwALT  44814  sspwtr  44817  pwtrVD  44820  pwtrrVD  44821  snssiALTVD  44823  sstrALT2VD  44830  suctrALT2VD  44832  elex2VD  44834  elex22VD  44835  eqsbc2VD  44836  tpid3gVD  44838  en3lplem1VD  44839  en3lplem2VD  44840  3ornot23VD  44843  orbi1rVD  44844  19.21a3con13vVD  44848  exbirVD  44849  exbiriVD  44850  rspsbc2VD  44851  tratrbVD  44857  syl5impVD  44859  ssralv2VD  44862  imbi12VD  44869  imbi13VD  44870  sbcim2gVD  44871  sbcbiVD  44872  truniALTVD  44874  trintALTVD  44876  onfrALTVD  44887  relopabVD  44897  19.41rgVD  44898  hbimpgVD  44900  ax6e2eqVD  44903  ax6e2ndeqVD  44905  con3ALTVD  44912