Theorem in2 43366

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

Syntax hints:   → wi 4  (   wvd1 43330  (   wvd2 43338

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 206  df-an 398  df-vd1 43331  df-vd2 43339

This theorem is referenced by:  e223  43396  trsspwALT  43579  sspwtr  43582  pwtrVD  43585  pwtrrVD  43586  snssiALTVD  43588  sstrALT2VD  43595  suctrALT2VD  43597  elex2VD  43599  elex22VD  43600  eqsbc2VD  43601  tpid3gVD  43603  en3lplem1VD  43604  en3lplem2VD  43605  3ornot23VD  43608  orbi1rVD  43609  19.21a3con13vVD  43613  exbirVD  43614  exbiriVD  43615  rspsbc2VD  43616  tratrbVD  43622  syl5impVD  43624  ssralv2VD  43627  imbi12VD  43634  imbi13VD  43635  sbcim2gVD  43636  sbcbiVD  43637  truniALTVD  43639  trintALTVD  43641  onfrALTVD  43652  relopabVD  43662  19.41rgVD  43663  hbimpgVD  43665  ax6e2eqVD  43668  ax6e2ndeqVD  43670  con3ALTVD  43677