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

Theorem in2 28643
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 28614 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32dfvd1ir 28601 1  |-  (. ph  ->.  ( ps  ->  ch ) ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28597   (.wvd2 28606
This theorem is referenced by:  e223  28673  trsspwALT  28868  sspwtr  28871  pwtrVD  28874  pwtrrVD  28875  snssiALTVD  28876  sstrALT2VD  28883  suctrALT2VD  28885  elex2VD  28887  elex22VD  28888  eqsbc3rVD  28889  tpid3gVD  28891  en3lplem1VD  28892  en3lplem2VD  28893  3ornot23VD  28896  orbi1rVD  28897  19.21a3con13vVD  28901  exbirVD  28902  exbiriVD  28903  rspsbc2VD  28904  tratrbVD  28910  syl5impVD  28912  ssralv2VD  28915  imbi12VD  28922  imbi13VD  28923  sbcim2gVD  28924  sbcbiVD  28925  truniALTVD  28927  trintALTVD  28929  onfrALTVD  28940  relopabVD  28950  19.41rgVD  28951  hbimpgVD  28953  a9e2eqVD  28956  a9e2ndeqVD  28958  con3ALTVD  28965
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 28598  df-vd2 28607
  Copyright terms: Public domain W3C validator