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

Theorem in2 36621
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 36592 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32dfvd1ir 36580 1  |-  (. ph  ->.  ( ps  ->  ch ) ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36576   (.wvd2 36584
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 188  df-an 372  df-vd1 36577  df-vd2 36585
This theorem is referenced by:  e223  36651  trsspwALT  36845  sspwtr  36848  pwtrVD  36859  pwtrrVD  36860  snssiALTVD  36862  sstrALT2VD  36869  suctrALT2VD  36871  elex2VD  36873  elex22VD  36874  eqsbc3rVD  36875  tpid3gVD  36877  en3lplem1VD  36878  en3lplem2VD  36879  3ornot23VD  36882  orbi1rVD  36883  19.21a3con13vVD  36887  exbirVD  36888  exbiriVD  36889  rspsbc2VD  36890  tratrbVD  36897  syl5impVD  36899  ssralv2VD  36902  imbi12VD  36909  imbi13VD  36910  sbcim2gVD  36911  sbcbiVD  36912  truniALTVD  36914  trintALTVD  36916  onfrALTVD  36927  relopabVD  36937  19.41rgVD  36938  hbimpgVD  36940  ax6e2eqVD  36943  ax6e2ndeqVD  36945  con3ALTVD  36952
  Copyright terms: Public domain W3C validator