Theorem in2 45032

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

Syntax hints:   → wi 4  (   wvd1 44996  (   wvd2 45004

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 44997  df-vd2 45005

This theorem is referenced by:  e223  45062  trsspwALT  45244  sspwtr  45247  pwtrVD  45250  pwtrrVD  45251  snssiALTVD  45253  sstrALT2VD  45260  suctrALT2VD  45262  elex2VD  45264  elex22VD  45265  eqsbc2VD  45266  tpid3gVD  45268  en3lplem1VD  45269  en3lplem2VD  45270  3ornot23VD  45273  orbi1rVD  45274  19.21a3con13vVD  45278  exbirVD  45279  exbiriVD  45280  rspsbc2VD  45281  tratrbVD  45287  syl5impVD  45289  ssralv2VD  45292  imbi12VD  45299  imbi13VD  45300  sbcim2gVD  45301  sbcbiVD  45302  truniALTVD  45304  trintALTVD  45306  onfrALTVD  45317  relopabVD  45327  19.41rgVD  45328  hbimpgVD  45330  ax6e2eqVD  45333  ax6e2ndeqVD  45335  con3ALTVD  45342