Theorem in2 44722

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

Syntax hints:   → wi 4  (   wvd1 44686  (   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-vd1 44687  df-vd2 44695

This theorem is referenced by:  e223  44752  trsspwALT  44934  sspwtr  44937  pwtrVD  44940  pwtrrVD  44941  snssiALTVD  44943  sstrALT2VD  44950  suctrALT2VD  44952  elex2VD  44954  elex22VD  44955  eqsbc2VD  44956  tpid3gVD  44958  en3lplem1VD  44959  en3lplem2VD  44960  3ornot23VD  44963  orbi1rVD  44964  19.21a3con13vVD  44968  exbirVD  44969  exbiriVD  44970  rspsbc2VD  44971  tratrbVD  44977  syl5impVD  44979  ssralv2VD  44982  imbi12VD  44989  imbi13VD  44990  sbcim2gVD  44991  sbcbiVD  44992  truniALTVD  44994  trintALTVD  44996  onfrALTVD  45007  relopabVD  45017  19.41rgVD  45018  hbimpgVD  45020  ax6e2eqVD  45023  ax6e2ndeqVD  45025  con3ALTVD  45032