Theorem in2 45297

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

Syntax hints:   → wi 4  (   wvd1 45261  (   wvd2 45269

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 45262  df-vd2 45270

This theorem is referenced by:  e223  45327  trsspwALT  45509  sspwtr  45512  pwtrVD  45515  pwtrrVD  45516  snssiALTVD  45518  sstrALT2VD  45525  suctrALT2VD  45527  elex2VD  45529  elex22VD  45530  eqsbc2VD  45531  tpid3gVD  45533  en3lplem1VD  45534  en3lplem2VD  45535  3ornot23VD  45538  orbi1rVD  45539  19.21a3con13vVD  45543  exbirVD  45544  exbiriVD  45545  rspsbc2VD  45546  tratrbVD  45552  syl5impVD  45554  ssralv2VD  45557  imbi12VD  45564  imbi13VD  45565  sbcim2gVD  45566  sbcbiVD  45567  truniALTVD  45569  trintALTVD  45571  onfrALTVD  45582  relopabVD  45592  19.41rgVD  45593  hbimpgVD  45595  ax6e2eqVD  45598  ax6e2ndeqVD  45600  con3ALTVD  45607