Theorem in2 44576

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

Syntax hints:   → wi 4  (   wvd1 44540  (   wvd2 44548

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 207  df-an 396  df-vd1 44541  df-vd2 44549

This theorem is referenced by:  e223  44606  trsspwALT  44789  sspwtr  44792  pwtrVD  44795  pwtrrVD  44796  snssiALTVD  44798  sstrALT2VD  44805  suctrALT2VD  44807  elex2VD  44809  elex22VD  44810  eqsbc2VD  44811  tpid3gVD  44813  en3lplem1VD  44814  en3lplem2VD  44815  3ornot23VD  44818  orbi1rVD  44819  19.21a3con13vVD  44823  exbirVD  44824  exbiriVD  44825  rspsbc2VD  44826  tratrbVD  44832  syl5impVD  44834  ssralv2VD  44837  imbi12VD  44844  imbi13VD  44845  sbcim2gVD  44846  sbcbiVD  44847  truniALTVD  44849  trintALTVD  44851  onfrALTVD  44862  relopabVD  44872  19.41rgVD  44873  hbimpgVD  44875  ax6e2eqVD  44878  ax6e2ndeqVD  44880  con3ALTVD  44887