Theorem in2 44842

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

Syntax hints:   → wi 4  (   wvd1 44806  (   wvd2 44814

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 44807  df-vd2 44815

This theorem is referenced by:  e223  44872  trsspwALT  45054  sspwtr  45057  pwtrVD  45060  pwtrrVD  45061  snssiALTVD  45063  sstrALT2VD  45070  suctrALT2VD  45072  elex2VD  45074  elex22VD  45075  eqsbc2VD  45076  tpid3gVD  45078  en3lplem1VD  45079  en3lplem2VD  45080  3ornot23VD  45083  orbi1rVD  45084  19.21a3con13vVD  45088  exbirVD  45089  exbiriVD  45090  rspsbc2VD  45091  tratrbVD  45097  syl5impVD  45099  ssralv2VD  45102  imbi12VD  45109  imbi13VD  45110  sbcim2gVD  45111  sbcbiVD  45112  truniALTVD  45114  trintALTVD  45116  onfrALTVD  45127  relopabVD  45137  19.41rgVD  45138  hbimpgVD  45140  ax6e2eqVD  45143  ax6e2ndeqVD  45145  con3ALTVD  45152