Theorem in2 37851

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

Syntax hints:   → wi 4  (   wvd1 37806  (   wvd2 37814

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 196  df-an 385  df-vd1 37807  df-vd2 37815

This theorem is referenced by:  e223  37881  trsspwALT  38067  sspwtr  38070  pwtrVD  38081  pwtrrVD  38082  snssiALTVD  38084  sstrALT2VD  38091  suctrALT2VD  38093  elex2VD  38095  elex22VD  38096  eqsbc3rVD  38097  tpid3gVD  38099  en3lplem1VD  38100  en3lplem2VD  38101  3ornot23VD  38104  orbi1rVD  38105  19.21a3con13vVD  38109  exbirVD  38110  exbiriVD  38111  rspsbc2VD  38112  tratrbVD  38119  syl5impVD  38121  ssralv2VD  38124  imbi12VD  38131  imbi13VD  38132  sbcim2gVD  38133  sbcbiVD  38134  truniALTVD  38136  trintALTVD  38138  onfrALTVD  38149  relopabVD  38159  19.41rgVD  38160  hbimpgVD  38162  ax6e2eqVD  38165  ax6e2ndeqVD  38167  con3ALTVD  38174