Theorem in2 44955

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

Syntax hints:   → wi 4  (   wvd1 44919  (   wvd2 44927

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 44920  df-vd2 44928

This theorem is referenced by:  e223  44985  trsspwALT  45167  sspwtr  45170  pwtrVD  45173  pwtrrVD  45174  snssiALTVD  45176  sstrALT2VD  45183  suctrALT2VD  45185  elex2VD  45187  elex22VD  45188  eqsbc2VD  45189  tpid3gVD  45191  en3lplem1VD  45192  en3lplem2VD  45193  3ornot23VD  45196  orbi1rVD  45197  19.21a3con13vVD  45201  exbirVD  45202  exbiriVD  45203  rspsbc2VD  45204  tratrbVD  45210  syl5impVD  45212  ssralv2VD  45215  imbi12VD  45222  imbi13VD  45223  sbcim2gVD  45224  sbcbiVD  45225  truniALTVD  45227  trintALTVD  45229  onfrALTVD  45240  relopabVD  45250  19.41rgVD  45251  hbimpgVD  45253  ax6e2eqVD  45256  ax6e2ndeqVD  45258  con3ALTVD  45265