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

Theorem in2 33731
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 33702 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32dfvd1ir 33690 1  |-  (. ph  ->.  ( ps  ->  ch ) ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 33686   (.wvd2 33694
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 369  df-vd1 33687  df-vd2 33695
This theorem is referenced by:  e223  33761  trsspwALT  33956  sspwtr  33959  pwtrVD  33970  pwtrrVD  33971  snssiALTVD  33973  sstrALT2VD  33980  suctrALT2VD  33982  elex2VD  33984  elex22VD  33985  eqsbc3rVD  33986  tpid3gVD  33988  en3lplem1VD  33989  en3lplem2VD  33990  3ornot23VD  33993  orbi1rVD  33994  19.21a3con13vVD  33998  exbirVD  33999  exbiriVD  34000  rspsbc2VD  34001  tratrbVD  34008  syl5impVD  34010  ssralv2VD  34013  imbi12VD  34020  imbi13VD  34021  sbcim2gVD  34022  sbcbiVD  34023  truniALTVD  34025  trintALTVD  34027  onfrALTVD  34038  relopabVD  34048  19.41rgVD  34049  hbimpgVD  34051  ax6e2eqVD  34054  ax6e2ndeqVD  34056  con3ALTVD  34063
  Copyright terms: Public domain W3C validator