Theorem in2 40932

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

Syntax hints:   → wi 4  (   wvd1 40896  (   wvd2 40904

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 209  df-an 399  df-vd1 40897  df-vd2 40905

This theorem is referenced by:  e223  40962  trsspwALT  41145  sspwtr  41148  pwtrVD  41151  pwtrrVD  41152  snssiALTVD  41154  sstrALT2VD  41161  suctrALT2VD  41163  elex2VD  41165  elex22VD  41166  eqsbc3rVD  41167  tpid3gVD  41169  en3lplem1VD  41170  en3lplem2VD  41171  3ornot23VD  41174  orbi1rVD  41175  19.21a3con13vVD  41179  exbirVD  41180  exbiriVD  41181  rspsbc2VD  41182  tratrbVD  41188  syl5impVD  41190  ssralv2VD  41193  imbi12VD  41200  imbi13VD  41201  sbcim2gVD  41202  sbcbiVD  41203  truniALTVD  41205  trintALTVD  41207  onfrALTVD  41218  relopabVD  41228  19.41rgVD  41229  hbimpgVD  41231  ax6e2eqVD  41234  ax6e2ndeqVD  41236  con3ALTVD  41243