Theorem in2 40937

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

Syntax hints:   → wi 4  (   wvd1 40901  (   wvd2 40909

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 209  df-an 399  df-vd1 40902  df-vd2 40910

This theorem is referenced by:  e223  40967  trsspwALT  41150  sspwtr  41153  pwtrVD  41156  pwtrrVD  41157  snssiALTVD  41159  sstrALT2VD  41166  suctrALT2VD  41168  elex2VD  41170  elex22VD  41171  eqsbc3rVD  41172  tpid3gVD  41174  en3lplem1VD  41175  en3lplem2VD  41176  3ornot23VD  41179  orbi1rVD  41180  19.21a3con13vVD  41184  exbirVD  41185  exbiriVD  41186  rspsbc2VD  41187  tratrbVD  41193  syl5impVD  41195  ssralv2VD  41198  imbi12VD  41205  imbi13VD  41206  sbcim2gVD  41207  sbcbiVD  41208  truniALTVD  41210  trintALTVD  41212  onfrALTVD  41223  relopabVD  41233  19.41rgVD  41234  hbimpgVD  41236  ax6e2eqVD  41239  ax6e2ndeqVD  41241  con3ALTVD  41248