Theorem in2 44712

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

Syntax hints:   → wi 4  (   wvd1 44676  (   wvd2 44684

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 44677  df-vd2 44685

This theorem is referenced by:  e223  44742  trsspwALT  44924  sspwtr  44927  pwtrVD  44930  pwtrrVD  44931  snssiALTVD  44933  sstrALT2VD  44940  suctrALT2VD  44942  elex2VD  44944  elex22VD  44945  eqsbc2VD  44946  tpid3gVD  44948  en3lplem1VD  44949  en3lplem2VD  44950  3ornot23VD  44953  orbi1rVD  44954  19.21a3con13vVD  44958  exbirVD  44959  exbiriVD  44960  rspsbc2VD  44961  tratrbVD  44967  syl5impVD  44969  ssralv2VD  44972  imbi12VD  44979  imbi13VD  44980  sbcim2gVD  44981  sbcbiVD  44982  truniALTVD  44984  trintALTVD  44986  onfrALTVD  44997  relopabVD  45007  19.41rgVD  45008  hbimpgVD  45010  ax6e2eqVD  45013  ax6e2ndeqVD  45015  con3ALTVD  45022