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

Theorem in3 28710
Description: The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
in3.1  |-  (. ph ,. ps ,. ch  ->.  th ).
Assertion
Ref Expression
in3  |-  (. ph ,. ps  ->.  ( ch  ->  th ) ).

Proof of Theorem in3
StepHypRef Expression
1 in3.1 . . 3  |-  (. ph ,. ps ,. ch  ->.  th ).
21dfvd3i 28684 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32dfvd2ir 28678 1  |-  (. ph ,. ps  ->.  ( ch  ->  th ) ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28669   (.wvd3 28679
This theorem is referenced by:  e223  28736  suctrALT2VD  28948  en3lplem2VD  28956  exbirVD  28965  exbiriVD  28966  rspsbc2VD  28967  tratrbVD  28973  ssralv2VD  28978  imbi12VD  28985  imbi13VD  28986  truniALTVD  28990  trintALTVD  28992  onfrALTlem2VD  29001
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-vd2 28670  df-vd3 28682
  Copyright terms: Public domain W3C validator