Theorem in2 38830

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

Syntax hints:   → wi 4  (   wvd1 38785  (   wvd2 38793

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 386  df-vd1 38786  df-vd2 38794

This theorem is referenced by:  e223  38860  trsspwALT  39045  sspwtr  39048  pwtrVD  39059  pwtrrVD  39060  snssiALTVD  39062  sstrALT2VD  39069  suctrALT2VD  39071  elex2VD  39073  elex22VD  39074  eqsbc3rVD  39075  tpid3gVD  39077  en3lplem1VD  39078  en3lplem2VD  39079  3ornot23VD  39082  orbi1rVD  39083  19.21a3con13vVD  39087  exbirVD  39088  exbiriVD  39089  rspsbc2VD  39090  tratrbVD  39097  syl5impVD  39099  ssralv2VD  39102  imbi12VD  39109  imbi13VD  39110  sbcim2gVD  39111  sbcbiVD  39112  truniALTVD  39114  trintALTVD  39116  onfrALTVD  39127  relopabVD  39137  19.41rgVD  39138  hbimpgVD  39140  ax6e2eqVD  39143  ax6e2ndeqVD  39145  con3ALTVD  39152