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

Theorem in2 28048
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 28019 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32dfvd1ir 28006 1  |-  (. ph  ->.  ( ps  ->  ch ) ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28002   (.wvd2 28011
This theorem is referenced by:  e223  28078  trsspwALT  28273  sspwtr  28276  pwtrVD  28279  pwtrrVD  28280  snssiALTVD  28281  sstrALT2VD  28288  suctrALT2VD  28290  elex2VD  28292  elex22VD  28293  eqsbc3rVD  28294  tpid3gVD  28296  en3lplem1VD  28297  en3lplem2VD  28298  3ornot23VD  28301  orbi1rVD  28302  19.21a3con13vVD  28306  exbirVD  28307  exbiriVD  28308  rspsbc2VD  28309  tratrbVD  28315  syl5impVD  28317  ssralv2VD  28320  imbi12VD  28327  imbi13VD  28328  sbcim2gVD  28329  sbcbiVD  28330  truniALTVD  28332  trintALTVD  28334  onfrALTVD  28345  relopabVD  28355  19.41rgVD  28356  hbimpgVD  28358  a9e2eqVD  28361  a9e2ndeqVD  28363  con3ALTVD  28370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-vd1 28003  df-vd2 28012
  Copyright terms: Public domain W3C validator