Theorem in2 45141

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

Syntax hints:   → wi 4  (   wvd1 45105  (   wvd2 45113

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 209  df-an 400  df-vd1 45106  df-vd2 45114

This theorem is referenced by:  e223  45171  trsspwALT  45353  sspwtr  45356  pwtrVD  45359  pwtrrVD  45360  snssiALTVD  45362  sstrALT2VD  45369  suctrALT2VD  45371  elex2VD  45373  elex22VD  45374  eqsbc2VD  45375  tpid3gVD  45377  en3lplem1VD  45378  en3lplem2VD  45379  3ornot23VD  45382  orbi1rVD  45383  19.21a3con13vVD  45387  exbirVD  45388  exbiriVD  45389  rspsbc2VD  45390  tratrbVD  45396  syl5impVD  45398  ssralv2VD  45401  imbi12VD  45408  imbi13VD  45409  sbcim2gVD  45410  sbcbiVD  45411  truniALTVD  45413  trintALTVD  45415  onfrALTVD  45426  relopabVD  45436  19.41rgVD  45437  hbimpgVD  45439  ax6e2eqVD  45442  ax6e2ndeqVD  45444  con3ALTVD  45451