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

Theorem in2 32346
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 32317 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32dfvd1ir 32305 1  |-  (. ph  ->.  ( ps  ->  ch ) ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 32301   (.wvd2 32309
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 32302  df-vd2 32310
This theorem is referenced by:  e223  32376  trsspwALT  32571  sspwtr  32574  pwtrVD  32579  pwtrrVD  32580  snssiALTVD  32582  sstrALT2VD  32589  suctrALT2VD  32591  elex2VD  32593  elex22VD  32594  eqsbc3rVD  32595  tpid3gVD  32597  en3lplem1VD  32598  en3lplem2VD  32599  3ornot23VD  32602  orbi1rVD  32603  19.21a3con13vVD  32607  exbirVD  32608  exbiriVD  32609  rspsbc2VD  32610  tratrbVD  32616  syl5impVD  32618  ssralv2VD  32621  imbi12VD  32628  imbi13VD  32629  sbcim2gVD  32630  sbcbiVD  32631  truniALTVD  32633  trintALTVD  32635  onfrALTVD  32646  relopabVD  32656  19.41rgVD  32657  hbimpgVD  32659  ax6e2eqVD  32662  ax6e2ndeqVD  32664  con3ALTVD  32671
  Copyright terms: Public domain W3C validator