Theorem in2 42225

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

Syntax hints:   → wi 4  (   wvd1 42189  (   wvd2 42197

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 206  df-an 397  df-vd1 42190  df-vd2 42198

This theorem is referenced by:  e223  42255  trsspwALT  42438  sspwtr  42441  pwtrVD  42444  pwtrrVD  42445  snssiALTVD  42447  sstrALT2VD  42454  suctrALT2VD  42456  elex2VD  42458  elex22VD  42459  eqsbc2VD  42460  tpid3gVD  42462  en3lplem1VD  42463  en3lplem2VD  42464  3ornot23VD  42467  orbi1rVD  42468  19.21a3con13vVD  42472  exbirVD  42473  exbiriVD  42474  rspsbc2VD  42475  tratrbVD  42481  syl5impVD  42483  ssralv2VD  42486  imbi12VD  42493  imbi13VD  42494  sbcim2gVD  42495  sbcbiVD  42496  truniALTVD  42498  trintALTVD  42500  onfrALTVD  42511  relopabVD  42521  19.41rgVD  42522  hbimpgVD  42524  ax6e2eqVD  42527  ax6e2ndeqVD  42529  con3ALTVD  42536