Theorem in2 45355

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45319  (   wvd2 45327

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-vd1 45320  df-vd2 45328

This theorem is used by:  e223  45385  trsspwALT  45567  sspwtr  45570  pwtrVD  45573  pwtrrVD  45574  snssiALTVD  45576  sstrALT2VD  45583  suctrALT2VD  45585  elex2VD  45587  elex22VD  45588  eqsbc2VD  45589  tpid3gVD  45591  en3lplem1VD  45592  en3lplem2VD  45593  3ornot23VD  45596  orbi1rVD  45597  19.21a3con13vVD  45601  exbirVD  45602  exbiriVD  45603  rspsbc2VD  45604  tratrbVD  45610  syl5impVD  45612  ssralv2VD  45615  imbi12VD  45622  imbi13VD  45623  sbcim2gVD  45624  sbcbiVD  45625  truniALTVD  45627  trintALTVD  45629  onfrALTVD  45640  relopabVD  45650  19.41rgVD  45651  hbimpgVD  45653  ax6e2eqVD  45656  ax6e2ndeqVD  45658  con3ALTVD  45665