Theorem in2 44579

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

Syntax hints:   → wi 4  (   wvd1 44543  (   wvd2 44551

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 44544  df-vd2 44552

This theorem is referenced by:  e223  44609  trsspwALT  44791  sspwtr  44794  pwtrVD  44797  pwtrrVD  44798  snssiALTVD  44800  sstrALT2VD  44807  suctrALT2VD  44809  elex2VD  44811  elex22VD  44812  eqsbc2VD  44813  tpid3gVD  44815  en3lplem1VD  44816  en3lplem2VD  44817  3ornot23VD  44820  orbi1rVD  44821  19.21a3con13vVD  44825  exbirVD  44826  exbiriVD  44827  rspsbc2VD  44828  tratrbVD  44834  syl5impVD  44836  ssralv2VD  44839  imbi12VD  44846  imbi13VD  44847  sbcim2gVD  44848  sbcbiVD  44849  truniALTVD  44851  trintALTVD  44853  onfrALTVD  44864  relopabVD  44874  19.41rgVD  44875  hbimpgVD  44877  ax6e2eqVD  44880  ax6e2ndeqVD  44882  con3ALTVD  44889