Theorem in2 44637

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

Syntax hints:   → wi 4  (   wvd1 44601  (   wvd2 44609

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 44602  df-vd2 44610

This theorem is referenced by:  e223  44667  trsspwALT  44849  sspwtr  44852  pwtrVD  44855  pwtrrVD  44856  snssiALTVD  44858  sstrALT2VD  44865  suctrALT2VD  44867  elex2VD  44869  elex22VD  44870  eqsbc2VD  44871  tpid3gVD  44873  en3lplem1VD  44874  en3lplem2VD  44875  3ornot23VD  44878  orbi1rVD  44879  19.21a3con13vVD  44883  exbirVD  44884  exbiriVD  44885  rspsbc2VD  44886  tratrbVD  44892  syl5impVD  44894  ssralv2VD  44897  imbi12VD  44904  imbi13VD  44905  sbcim2gVD  44906  sbcbiVD  44907  truniALTVD  44909  trintALTVD  44911  onfrALTVD  44922  relopabVD  44932  19.41rgVD  44933  hbimpgVD  44935  ax6e2eqVD  44938  ax6e2ndeqVD  44940  con3ALTVD  44947