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

Theorem in2 33119
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 33090 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32dfvd1ir 33078 1  |-  (. ph  ->.  ( ps  ->  ch ) ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 33074   (.wvd2 33082
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 33075  df-vd2 33083
This theorem is referenced by:  e223  33149  trsspwALT  33344  sspwtr  33347  pwtrVD  33352  pwtrrVD  33353  snssiALTVD  33355  sstrALT2VD  33362  suctrALT2VD  33364  elex2VD  33366  elex22VD  33367  eqsbc3rVD  33368  tpid3gVD  33370  en3lplem1VD  33371  en3lplem2VD  33372  3ornot23VD  33375  orbi1rVD  33376  19.21a3con13vVD  33380  exbirVD  33381  exbiriVD  33382  rspsbc2VD  33383  tratrbVD  33389  syl5impVD  33391  ssralv2VD  33394  imbi12VD  33401  imbi13VD  33402  sbcim2gVD  33403  sbcbiVD  33404  truniALTVD  33406  trintALTVD  33408  onfrALTVD  33419  relopabVD  33429  19.41rgVD  33430  hbimpgVD  33432  ax6e2eqVD  33435  ax6e2ndeqVD  33437  con3ALTVD  33444
  Copyright terms: Public domain W3C validator