Theorem in2 45056

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

Syntax hints:   → wi 4  (   wvd1 45020  (   wvd2 45028

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 45021  df-vd2 45029

This theorem is referenced by:  e223  45086  trsspwALT  45268  sspwtr  45271  pwtrVD  45274  pwtrrVD  45275  snssiALTVD  45277  sstrALT2VD  45284  suctrALT2VD  45286  elex2VD  45288  elex22VD  45289  eqsbc2VD  45290  tpid3gVD  45292  en3lplem1VD  45293  en3lplem2VD  45294  3ornot23VD  45297  orbi1rVD  45298  19.21a3con13vVD  45302  exbirVD  45303  exbiriVD  45304  rspsbc2VD  45305  tratrbVD  45311  syl5impVD  45313  ssralv2VD  45316  imbi12VD  45323  imbi13VD  45324  sbcim2gVD  45325  sbcbiVD  45326  truniALTVD  45328  trintALTVD  45330  onfrALTVD  45341  relopabVD  45351  19.41rgVD  45352  hbimpgVD  45354  ax6e2eqVD  45357  ax6e2ndeqVD  45359  con3ALTVD  45366