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 39516
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 39487 . 2 (𝜑 → (𝜓𝜒))
32dfvd1ir 39475 1 (   𝜑   ▶   (𝜓𝜒)   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 39471  (   wvd2 39479
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 198  df-an 385  df-vd1 39472  df-vd2 39480
This theorem is referenced by:  e223  39546  trsspwALT  39730  sspwtr  39733  pwtrVD  39736  pwtrrVD  39737  snssiALTVD  39739  sstrALT2VD  39746  suctrALT2VD  39748  elex2VD  39750  elex22VD  39751  eqsbc3rVD  39752  tpid3gVD  39754  en3lplem1VD  39755  en3lplem2VD  39756  3ornot23VD  39759  orbi1rVD  39760  19.21a3con13vVD  39764  exbirVD  39765  exbiriVD  39766  rspsbc2VD  39767  tratrbVD  39773  syl5impVD  39775  ssralv2VD  39778  imbi12VD  39785  imbi13VD  39786  sbcim2gVD  39787  sbcbiVD  39788  truniALTVD  39790  trintALTVD  39792  onfrALTVD  39803  relopabVD  39813  19.41rgVD  39814  hbimpgVD  39816  ax6e2eqVD  39819  ax6e2ndeqVD  39821  con3ALTVD  39828
  Copyright terms: Public domain W3C validator