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

Theorem in2 28682
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 28653 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32dfvd1ir 28640 1  |-  (. ph  ->.  ( ps  ->  ch ) ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28636   (.wvd2 28645
This theorem is referenced by:  e223  28712  trsspwALT  28908  sspwtr  28911  pwtrVD  28914  pwtrrVD  28916  snssiALTVD  28918  sstrALT2VD  28926  suctrALT2VD  28928  elex2VD  28930  elex22VD  28931  eqsbc3rVD  28932  tpid3gVD  28934  en3lplem1VD  28935  en3lplem2VD  28936  3ornot23VD  28939  orbi1rVD  28940  19.21a3con13vVD  28944  exbirVD  28945  exbiriVD  28946  rspsbc2VD  28947  tratrbVD  28953  syl5impVD  28955  ssralv2VD  28958  imbi12VD  28965  imbi13VD  28966  sbcim2gVD  28967  sbcbiVD  28968  truniALTVD  28970  trintALTVD  28972  onfrALTVD  28983  relopabVD  28993  19.41rgVD  28994  hbimpgVD  28996  a9e2eqVD  28999  a9e2ndeqVD  29001  con3ALTVD  29008
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 177  df-an 360  df-vd1 28637  df-vd2 28646
  Copyright terms: Public domain W3C validator