Theorem in2 45682

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45646  (   wvd2 45654

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 45647  df-vd2 45655

This theorem is used by:  e223  45712  trsspwALT  45894  sspwtr  45897  pwtrVD  45900  pwtrrVD  45901  snssiALTVD  45903  sstrALT2VD  45910  suctrALT2VD  45912  elex2VD  45914  elex22VD  45915  eqsbc2VD  45916  tpid3gVD  45918  en3lplem1VD  45919  en3lplem2VD  45920  3ornot23VD  45923  orbi1rVD  45924  19.21a3con13vVD  45928  exbirVD  45929  exbiriVD  45930  rspsbc2VD  45931  tratrbVD  45937  syl5impVD  45939  ssralv2VD  45942  imbi12VD  45949  imbi13VD  45950  sbcim2gVD  45951  sbcbiVD  45952  truniALTVD  45954  trintALTVD  45956  onfrALTVD  45967  relopabVD  45977  19.41rgVD  45978  hbimpgVD  45980  ax6e2eqVD  45983  ax6e2ndeqVD  45985  con3ALTVD  45992