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

Theorem in2 37026
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  |-  (. ph ,. ps  ->.  ch ).
Assertion
Ref Expression
in2  |-  (. ph  ->.  ( ps  ->  ch ) ).

Proof of Theorem in2
StepHypRef Expression
1 in2.1 . . 3  |-  (. ph ,. ps  ->.  ch ).
21dfvd2i 36997 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32dfvd1ir 36985 1  |-  (. ph  ->.  ( ps  ->  ch ) ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36981   (.wvd2 36989
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 190  df-an 377  df-vd1 36982  df-vd2 36990
This theorem is referenced by:  e223  37056  trsspwALT  37245  sspwtr  37248  pwtrVD  37259  pwtrrVD  37260  snssiALTVD  37262  sstrALT2VD  37269  suctrALT2VD  37271  elex2VD  37273  elex22VD  37274  eqsbc3rVD  37275  tpid3gVD  37277  en3lplem1VD  37278  en3lplem2VD  37279  3ornot23VD  37282  orbi1rVD  37283  19.21a3con13vVD  37287  exbirVD  37288  exbiriVD  37289  rspsbc2VD  37290  tratrbVD  37297  syl5impVD  37299  ssralv2VD  37302  imbi12VD  37309  imbi13VD  37310  sbcim2gVD  37311  sbcbiVD  37312  truniALTVD  37314  trintALTVD  37316  onfrALTVD  37327  relopabVD  37337  19.41rgVD  37338  hbimpgVD  37340  ax6e2eqVD  37343  ax6e2ndeqVD  37345  con3ALTVD  37352
  Copyright terms: Public domain W3C validator