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

Theorem in3 28381
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 28361 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32dfvd2ir 28355 1  |-  (. ph ,. ps  ->.  ( ch  ->  th ) ).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd2 28346   (.wvd3 28356
This theorem is referenced by:  e223  28407  suctrALT2VD  28612  en3lplem2VD  28620  exbirVD  28629  exbiriVD  28630  rspsbc2VD  28631  tratrbVD  28637  ssralv2VD  28642  imbi12VD  28649  imbi13VD  28650  truniALTVD  28654  trintALTVD  28656  onfrALTlem2VD  28665
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 28347  df-vd3 28359
  Copyright terms: Public domain W3C validator