Theorem in2 45050

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

Syntax hints:   → wi 4  (   wvd1 45014  (   wvd2 45022

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 45015  df-vd2 45023

This theorem is referenced by:  e223  45080  trsspwALT  45262  sspwtr  45265  pwtrVD  45268  pwtrrVD  45269  snssiALTVD  45271  sstrALT2VD  45278  suctrALT2VD  45280  elex2VD  45282  elex22VD  45283  eqsbc2VD  45284  tpid3gVD  45286  en3lplem1VD  45287  en3lplem2VD  45288  3ornot23VD  45291  orbi1rVD  45292  19.21a3con13vVD  45296  exbirVD  45297  exbiriVD  45298  rspsbc2VD  45299  tratrbVD  45305  syl5impVD  45307  ssralv2VD  45310  imbi12VD  45317  imbi13VD  45318  sbcim2gVD  45319  sbcbiVD  45320  truniALTVD  45322  trintALTVD  45324  onfrALTVD  45335  relopabVD  45345  19.41rgVD  45346  hbimpgVD  45348  ax6e2eqVD  45351  ax6e2ndeqVD  45353  con3ALTVD  45360