Theorem in2 45547

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45511  (   wvd2 45519

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 45512  df-vd2 45520

This theorem is used by:  e223  45577  trsspwALT  45759  sspwtr  45762  pwtrVD  45765  pwtrrVD  45766  snssiALTVD  45768  sstrALT2VD  45775  suctrALT2VD  45777  elex2VD  45779  elex22VD  45780  eqsbc2VD  45781  tpid3gVD  45783  en3lplem1VD  45784  en3lplem2VD  45785  3ornot23VD  45788  orbi1rVD  45789  19.21a3con13vVD  45793  exbirVD  45794  exbiriVD  45795  rspsbc2VD  45796  tratrbVD  45802  syl5impVD  45804  ssralv2VD  45807  imbi12VD  45814  imbi13VD  45815  sbcim2gVD  45816  sbcbiVD  45817  truniALTVD  45819  trintALTVD  45821  onfrALTVD  45832  relopabVD  45842  19.41rgVD  45843  hbimpgVD  45845  ax6e2eqVD  45848  ax6e2ndeqVD  45850  con3ALTVD  45857