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

Theorem in3 28686
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 28660 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32dfvd2ir 28654 1  |-  (. ph ,. ps  ->.  ( ch  ->  th ) ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28645   (.wvd3 28655
This theorem is referenced by:  e223  28712  suctrALT2VD  28928  en3lplem2VD  28936  exbirVD  28945  exbiriVD  28946  rspsbc2VD  28947  tratrbVD  28953  ssralv2VD  28958  imbi12VD  28965  imbi13VD  28966  truniALTVD  28970  trintALTVD  28972  onfrALTlem2VD  28981
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 177  df-an 360  df-3an 936  df-vd2 28646  df-vd3 28658
  Copyright terms: Public domain W3C validator