Theorem in2 45436

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45400  (   wvd2 45408

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-vd1 45401  df-vd2 45409

This theorem is used by:  e223  45466  trsspwALT  45648  sspwtr  45651  pwtrVD  45654  pwtrrVD  45655  snssiALTVD  45657  sstrALT2VD  45664  suctrALT2VD  45666  elex2VD  45668  elex22VD  45669  eqsbc2VD  45670  tpid3gVD  45672  en3lplem1VD  45673  en3lplem2VD  45674  3ornot23VD  45677  orbi1rVD  45678  19.21a3con13vVD  45682  exbirVD  45683  exbiriVD  45684  rspsbc2VD  45685  tratrbVD  45691  syl5impVD  45693  ssralv2VD  45696  imbi12VD  45703  imbi13VD  45704  sbcim2gVD  45705  sbcbiVD  45706  truniALTVD  45708  trintALTVD  45710  onfrALTVD  45721  relopabVD  45731  19.41rgVD  45732  hbimpgVD  45734  ax6e2eqVD  45737  ax6e2ndeqVD  45739  con3ALTVD  45746