Theorem in2 40499

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

Syntax hints:   → wi 4  (   wvd1 40463  (   wvd2 40471

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 208  df-an 397  df-vd1 40464  df-vd2 40472

This theorem is referenced by:  e223  40529  trsspwALT  40712  sspwtr  40715  pwtrVD  40718  pwtrrVD  40719  snssiALTVD  40721  sstrALT2VD  40728  suctrALT2VD  40730  elex2VD  40732  elex22VD  40733  eqsbc3rVD  40734  tpid3gVD  40736  en3lplem1VD  40737  en3lplem2VD  40738  3ornot23VD  40741  orbi1rVD  40742  19.21a3con13vVD  40746  exbirVD  40747  exbiriVD  40748  rspsbc2VD  40749  tratrbVD  40755  syl5impVD  40757  ssralv2VD  40760  imbi12VD  40767  imbi13VD  40768  sbcim2gVD  40769  sbcbiVD  40770  truniALTVD  40772  trintALTVD  40774  onfrALTVD  40785  relopabVD  40795  19.41rgVD  40796  hbimpgVD  40798  ax6e2eqVD  40801  ax6e2ndeqVD  40803  con3ALTVD  40810