Theorem in2 44603

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

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

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

This theorem is referenced by:  e223  44633  trsspwALT  44816  sspwtr  44819  pwtrVD  44822  pwtrrVD  44823  snssiALTVD  44825  sstrALT2VD  44832  suctrALT2VD  44834  elex2VD  44836  elex22VD  44837  eqsbc2VD  44838  tpid3gVD  44840  en3lplem1VD  44841  en3lplem2VD  44842  3ornot23VD  44845  orbi1rVD  44846  19.21a3con13vVD  44850  exbirVD  44851  exbiriVD  44852  rspsbc2VD  44853  tratrbVD  44859  syl5impVD  44861  ssralv2VD  44864  imbi12VD  44871  imbi13VD  44872  sbcim2gVD  44873  sbcbiVD  44874  truniALTVD  44876  trintALTVD  44878  onfrALTVD  44889  relopabVD  44899  19.41rgVD  44900  hbimpgVD  44902  ax6e2eqVD  44905  ax6e2ndeqVD  44907  con3ALTVD  44914