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

Theorem in2 31630
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 31601 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32dfvd1ir 31589 1  |-  (. ph  ->.  ( ps  ->  ch ) ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 31585   (.wvd2 31593
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 185  df-an 371  df-vd1 31586  df-vd2 31594
This theorem is referenced by:  e223  31660  trsspwALT  31855  sspwtr  31858  pwtrVD  31863  pwtrrVD  31864  snssiALTVD  31866  sstrALT2VD  31873  suctrALT2VD  31875  elex2VD  31877  elex22VD  31878  eqsbc3rVD  31879  tpid3gVD  31881  en3lplem1VD  31882  en3lplem2VD  31883  3ornot23VD  31886  orbi1rVD  31887  19.21a3con13vVD  31891  exbirVD  31892  exbiriVD  31893  rspsbc2VD  31894  tratrbVD  31900  syl5impVD  31902  ssralv2VD  31905  imbi12VD  31912  imbi13VD  31913  sbcim2gVD  31914  sbcbiVD  31915  truniALTVD  31917  trintALTVD  31919  onfrALTVD  31930  relopabVD  31940  19.41rgVD  31941  hbimpgVD  31943  ax6e2eqVD  31946  ax6e2ndeqVD  31948  con3ALTVD  31955
  Copyright terms: Public domain W3C validator