Theorem in2 44352

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

Syntax hints:   → wi 4  (   wvd1 44316  (   wvd2 44324

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 395  df-vd1 44317  df-vd2 44325

This theorem is referenced by:  e223  44382  trsspwALT  44565  sspwtr  44568  pwtrVD  44571  pwtrrVD  44572  snssiALTVD  44574  sstrALT2VD  44581  suctrALT2VD  44583  elex2VD  44585  elex22VD  44586  eqsbc2VD  44587  tpid3gVD  44589  en3lplem1VD  44590  en3lplem2VD  44591  3ornot23VD  44594  orbi1rVD  44595  19.21a3con13vVD  44599  exbirVD  44600  exbiriVD  44601  rspsbc2VD  44602  tratrbVD  44608  syl5impVD  44610  ssralv2VD  44613  imbi12VD  44620  imbi13VD  44621  sbcim2gVD  44622  sbcbiVD  44623  truniALTVD  44625  trintALTVD  44627  onfrALTVD  44638  relopabVD  44648  19.41rgVD  44649  hbimpgVD  44651  ax6e2eqVD  44654  ax6e2ndeqVD  44656  con3ALTVD  44663