Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  in2 Structured version   Visualization version   GIF version

Theorem in2 44625
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
StepHypRef Expression
1 in2.1 . . 3 (   𝜑   ,   𝜓   ▶   𝜒   )
21dfvd2i 44605 . 2 (𝜑 → (𝜓𝜒))
32dfvd1ir 44593 1 (   𝜑   ▶   (𝜓𝜒)   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 44589  (   wvd2 44597
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 44590  df-vd2 44598
This theorem is referenced by:  e223  44655  trsspwALT  44838  sspwtr  44841  pwtrVD  44844  pwtrrVD  44845  snssiALTVD  44847  sstrALT2VD  44854  suctrALT2VD  44856  elex2VD  44858  elex22VD  44859  eqsbc2VD  44860  tpid3gVD  44862  en3lplem1VD  44863  en3lplem2VD  44864  3ornot23VD  44867  orbi1rVD  44868  19.21a3con13vVD  44872  exbirVD  44873  exbiriVD  44874  rspsbc2VD  44875  tratrbVD  44881  syl5impVD  44883  ssralv2VD  44886  imbi12VD  44893  imbi13VD  44894  sbcim2gVD  44895  sbcbiVD  44896  truniALTVD  44898  trintALTVD  44900  onfrALTVD  44911  relopabVD  44921  19.41rgVD  44922  hbimpgVD  44924  ax6e2eqVD  44927  ax6e2ndeqVD  44929  con3ALTVD  44936
  Copyright terms: Public domain W3C validator