Theorem in2 44595

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

Syntax hints:   → wi 4  (   wvd1 44559  (   wvd2 44567

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 44560  df-vd2 44568

This theorem is referenced by:  e223  44625  trsspwALT  44807  sspwtr  44810  pwtrVD  44813  pwtrrVD  44814  snssiALTVD  44816  sstrALT2VD  44823  suctrALT2VD  44825  elex2VD  44827  elex22VD  44828  eqsbc2VD  44829  tpid3gVD  44831  en3lplem1VD  44832  en3lplem2VD  44833  3ornot23VD  44836  orbi1rVD  44837  19.21a3con13vVD  44841  exbirVD  44842  exbiriVD  44843  rspsbc2VD  44844  tratrbVD  44850  syl5impVD  44852  ssralv2VD  44855  imbi12VD  44862  imbi13VD  44863  sbcim2gVD  44864  sbcbiVD  44865  truniALTVD  44867  trintALTVD  44869  onfrALTVD  44880  relopabVD  44890  19.41rgVD  44891  hbimpgVD  44893  ax6e2eqVD  44896  ax6e2ndeqVD  44898  con3ALTVD  44905