Theorem in2 44597

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

Syntax hints:   → wi 4  (   wvd1 44561  (   wvd2 44569

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 44562  df-vd2 44570

This theorem is referenced by:  e223  44627  trsspwALT  44809  sspwtr  44812  pwtrVD  44815  pwtrrVD  44816  snssiALTVD  44818  sstrALT2VD  44825  suctrALT2VD  44827  elex2VD  44829  elex22VD  44830  eqsbc2VD  44831  tpid3gVD  44833  en3lplem1VD  44834  en3lplem2VD  44835  3ornot23VD  44838  orbi1rVD  44839  19.21a3con13vVD  44843  exbirVD  44844  exbiriVD  44845  rspsbc2VD  44846  tratrbVD  44852  syl5impVD  44854  ssralv2VD  44857  imbi12VD  44864  imbi13VD  44865  sbcim2gVD  44866  sbcbiVD  44867  truniALTVD  44869  trintALTVD  44871  onfrALTVD  44882  relopabVD  44892  19.41rgVD  44893  hbimpgVD  44895  ax6e2eqVD  44898  ax6e2ndeqVD  44900  con3ALTVD  44907