Theorem in2 42535

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

Syntax hints:   → wi 4  (   wvd1 42499  (   wvd2 42507

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 397  df-vd1 42500  df-vd2 42508

This theorem is referenced by:  e223  42565  trsspwALT  42748  sspwtr  42751  pwtrVD  42754  pwtrrVD  42755  snssiALTVD  42757  sstrALT2VD  42764  suctrALT2VD  42766  elex2VD  42768  elex22VD  42769  eqsbc2VD  42770  tpid3gVD  42772  en3lplem1VD  42773  en3lplem2VD  42774  3ornot23VD  42777  orbi1rVD  42778  19.21a3con13vVD  42782  exbirVD  42783  exbiriVD  42784  rspsbc2VD  42785  tratrbVD  42791  syl5impVD  42793  ssralv2VD  42796  imbi12VD  42803  imbi13VD  42804  sbcim2gVD  42805  sbcbiVD  42806  truniALTVD  42808  trintALTVD  42810  onfrALTVD  42821  relopabVD  42831  19.41rgVD  42832  hbimpgVD  42834  ax6e2eqVD  42837  ax6e2ndeqVD  42839  con3ALTVD  42846