Theorem in2 45173

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

Syntax hints:   → wi 4  (   wvd1 45137  (   wvd2 45145

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 210  df-an 401  df-vd1 45138  df-vd2 45146

This theorem is referenced by:  e223  45203  trsspwALT  45385  sspwtr  45388  pwtrVD  45391  pwtrrVD  45392  snssiALTVD  45394  sstrALT2VD  45401  suctrALT2VD  45403  elex2VD  45405  elex22VD  45406  eqsbc2VD  45407  tpid3gVD  45409  en3lplem1VD  45410  en3lplem2VD  45411  3ornot23VD  45414  orbi1rVD  45415  19.21a3con13vVD  45419  exbirVD  45420  exbiriVD  45421  rspsbc2VD  45422  tratrbVD  45428  syl5impVD  45430  ssralv2VD  45433  imbi12VD  45440  imbi13VD  45441  sbcim2gVD  45442  sbcbiVD  45443  truniALTVD  45445  trintALTVD  45447  onfrALTVD  45458  relopabVD  45468  19.41rgVD  45469  hbimpgVD  45471  ax6e2eqVD  45474  ax6e2ndeqVD  45476  con3ALTVD  45483