Theorem in2 42114

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

Syntax hints:   → wi 4  (   wvd1 42078  (   wvd2 42086

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 396  df-vd1 42079  df-vd2 42087

This theorem is referenced by:  e223  42144  trsspwALT  42327  sspwtr  42330  pwtrVD  42333  pwtrrVD  42334  snssiALTVD  42336  sstrALT2VD  42343  suctrALT2VD  42345  elex2VD  42347  elex22VD  42348  eqsbc2VD  42349  tpid3gVD  42351  en3lplem1VD  42352  en3lplem2VD  42353  3ornot23VD  42356  orbi1rVD  42357  19.21a3con13vVD  42361  exbirVD  42362  exbiriVD  42363  rspsbc2VD  42364  tratrbVD  42370  syl5impVD  42372  ssralv2VD  42375  imbi12VD  42382  imbi13VD  42383  sbcim2gVD  42384  sbcbiVD  42385  truniALTVD  42387  trintALTVD  42389  onfrALTVD  42400  relopabVD  42410  19.41rgVD  42411  hbimpgVD  42413  ax6e2eqVD  42416  ax6e2ndeqVD  42418  con3ALTVD  42425