Theorem in2 39350

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

Syntax hints:   → wi 4  (   wvd1 39305  (   wvd2 39313

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 197  df-an 385  df-vd1 39306  df-vd2 39314

This theorem is referenced by:  e223  39380  trsspwALT  39565  sspwtr  39568  pwtrVD  39576  pwtrrVD  39577  snssiALTVD  39579  sstrALT2VD  39586  suctrALT2VD  39588  elex2VD  39590  elex22VD  39591  eqsbc3rVD  39592  tpid3gVD  39594  en3lplem1VD  39595  en3lplem2VD  39596  3ornot23VD  39599  orbi1rVD  39600  19.21a3con13vVD  39604  exbirVD  39605  exbiriVD  39606  rspsbc2VD  39607  tratrbVD  39614  syl5impVD  39616  ssralv2VD  39619  imbi12VD  39626  imbi13VD  39627  sbcim2gVD  39628  sbcbiVD  39629  truniALTVD  39631  trintALTVD  39633  onfrALTVD  39644  relopabVD  39654  19.41rgVD  39655  hbimpgVD  39657  ax6e2eqVD  39660  ax6e2ndeqVD  39662  con3ALTVD  39669