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

Theorem in2 28377
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 28354 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32dfvd1ir 28341 1  |-  (. ph  ->.  ( ps  ->  ch ) ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28337   (.wvd2 28346
This theorem is referenced by:  e223  28407  trsspwALT  28592  sspwtr  28595  pwtrVD  28598  pwtrrVD  28600  snssiALTVD  28602  sstrALT2VD  28610  suctrALT2VD  28612  elex2VD  28614  elex22VD  28615  eqsbc3rVD  28616  tpid3gVD  28618  en3lplem1VD  28619  en3lplem2VD  28620  3ornot23VD  28623  orbi1rVD  28624  19.21a3con13vVD  28628  exbirVD  28629  exbiriVD  28630  rspsbc2VD  28631  tratrbVD  28637  syl5impVD  28639  ssralv2VD  28642  imbi12VD  28649  imbi13VD  28650  sbcim2gVD  28651  sbcbiVD  28652  truniALTVD  28654  trintALTVD  28656  onfrALTVD  28667  relopabVD  28677  19.41rgVD  28678  hbimpgVD  28680  a9e2eqVD  28683  a9e2ndeqVD  28685  con3ALTVD  28692
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 28338  df-vd2 28347
  Copyright terms: Public domain W3C validator